最小不動点定理をfactを用いて確認する
最小不動点定理の再掲
定理
Dをcpo
fを連続関数D\to D
とする
あるa\in Dが存在して、以下の2つを満たす
f(a) =a
f(b)=bならば、a\sqsubseteq b
また、この最小不動点aは以下のように表せる
a = \sqcup\{f^n(\bot)\;|\;n\in\mathbb{N}\}
/mrsekut-book-4320026578/087では、具体例として階乗関数\Phi_\mathrm{fact}(\bot)が出てくる
まず、この\Phi_\mathrm{fact}をHaskellで定義すると以下のようになる
hsphi :: (Int -> Int) -> Int -> Int
phi f x = if x == 0 then 1 else x * f(x - 1)これが、上の定理のfの具体例になっている
この関数
phi は、階乗関数factを1段階メタにしたもの以下のようにして、段階ごとの部分関数factを定義できる
hsfact0 x = undefined
fact1 x = phi undefined x
fact2 x = (phi . phi) undefiend x
fact3 x = (phi . phi . phi) undefined x
fact4 x = (phi . phi . phi . phi) undefined x
...例えば、
fact4 の定義は以下のように書いているのと同じ\mathrm{fact4}(x) = \Phi^4_\mathrm{fact}(\bot)(x)
使用感はこうなる
hsfact4 0 -- 1
fact4 1 -- 1
fact4 2 -- 2
fact4 3 -- 6
fact4 4 -- error
fact4 5 -- error要は、
factn 関数は、 (n-1)! までを求められる部分関数になるこれを無限に続けていけば以下のようになるが、これは書けないので
hsfactInf x (phi . ... . phi) undefined x普通に再帰的に定義したfactで代用する
hsfactInf x = if x == 0 then 1 else x * factInf (x - 1)a = \sqcup\{f^n(\bot)\;|\;n\in\mathbb{N}\}となることを確認したい
これは、A=\{\bot,f(\bot),f(f(\bot)),f(f(f(\bot))),\cdots\}という集合があった時に、
その上限\sqcup Aが、fの最小不動点に等しくなる
ということを言っている
またこの関数は単調なので、不動点はこの最小不動点1つのみである
不動点が複数ある関数もある
ref 不動点が複数の関数である関数の例
最小の不動点が、上限であることが直観に反するポイントな感じがある
factの話でのAは、
A = {fact0, fact1, fact2, ... , factInf} という集合のことであるこれの上限は、もちろん
factInf であるということは、定理的には、
factInf が、 phi の最小不動点であるということを言っている
つまり以下が成り立つ
factInf == phi factInf 確認と言うには厳密性に欠けるが、実際
phi factInf は任意の自然数 x を引数にとって、 x! を求められるhsphi factInf 5 -- 120
phi factInf 10 -- 3628800
..また、不動点コンビネータであるfix関数を用いることで最小不動点が得られる
今回の場合は、
factInf == fix phi になるhsfix phi 5 -- 120
fix phi 10 -- 3628800
..