階乗関数fact
この辺の具体例を見るのに良い
階乗を求める関数 fact を考える
これは
部分関数の半順序集合\mathrm{Fun}(\mathbb{N},\mathbb{N})に含まれる関数である
普通に定義するとこうなる
hsfact :: Int -> Int
fact n = if n == 0 then 1 else n * fact (n - 1)
これを、再帰部分を展開して書くとこうなる
hsfact_inf n = if n == 0 then 1
else n * (if n - 1 == 0 then 1
else (n - 1) * (if n - 2 == 0 then 1
else ...))
これを\mathrm{fact}_\infinとする
この無限の展開を途中でやめた関数\mathrm{fact}_nを考える
hsfact1 n = if n == 0 then 1 else undefined
hsfact2 n = if n == 0 then 1
else n * (if n - 1 == 0 then 1 else undefined)
hsfact3 n = if n == 0 then 1
else n * (if n - 1 == 0 then 1
else (n - 1) * (if n - 2 == 0 then 1 else undefined))
..
これらは、
\mathrm{dom}(\mathrm{fact}_1)=\{0\}
\mathrm{dom}(\mathrm{fact}_2)=\{0,1\}
\mathrm{dom}(\mathrm{fact}_3)=\{0,1,2\}
..
のような部分関数になっている
この時、
\bot = \mathrm{fact}_0\sqsubseteq\mathrm{fact}_1\sqsubseteq \mathrm{fact}_2\sqsubseteq\mathrm{fact}_3\sqsubseteq\cdots\sqsubseteq \mathrm{fact}_\infinになる
集合P\{\mathrm{fact_1},\mathrm{fact_2},\cdots\}の上限は\mathrm{fact_\infin}
参考