階乗関数fact
この辺の具体例を見るのに良い
階乗を求める関数factを考える
これは部分関数の半順序集合$ \mathrm{Fun}(\mathbb{N},\mathbb{N})に含まれる関数である 普通に定義するとこうなる
code:hs
fact :: Int -> Int
fact n = if n == 0 then 1 else n * fact (n - 1)
これを、再帰部分を展開して書くとこうなる
code:hs
fact_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を考える
code:hs
fact1 n = if n == 0 then 1 else undefined
code:hs
fact2 n = if n == 0 then 1
else n * (if n - 1 == 0 then 1 else undefined)
code:hs
fact3 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}
参考