最小不動点定理を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で定義すると以下のようになる

code:hs

phi :: (Int -> Int) -> Int -> Int

phi f x = if x == 0 then 1 else x * f(x - 1)

これが、上の定理の$ fの具体例になっている

この関数phiは、階乗関数factを1段階メタにしたもの

以下のようにして、段階ごとの部分関数factを定義できる

code:hs

fact0 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)

使用感はこうなる

code:hs

fact4 0 -- 1

fact4 1 -- 1

fact4 2 -- 2

fact4 3 -- 6

fact4 4 -- error

fact4 5 -- error

要は、factn関数は、(n-1)!までを求められる部分関数になる

これを無限に続けていけば以下のようになるが、これは書けないので

code:hs

factInf x (phi . ... . phi) undefined x

普通に再帰的に定義したfactで代用する

code:hs

factInf 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 不動点が複数の関数である関数の例

最小の不動点が、上限であることが直観に反するポイントな感じがあるmrsekut.icon

factの話での$ Aは、

A = {fact0, fact1, fact2, ... , factInf}という集合のことである

これの上限は、もちろんfactInfである

ということは、定理的には、

factInfが、phiの最小不動点である

ということを言っている

つまり以下が成り立つ

factInf == phi factInf

確認と言うには厳密性に欠けるが、実際

phi factInfは任意の自然数xを引数にとって、x!を求められる

code:hs

phi factInf 5 -- 120

phi factInf 10 -- 3628800

また、不動点コンビネータであるfix関数を用いることで最小不動点が得られる

今回の場合は、factInf == fix phiになる

code:hs

fix phi 5 -- 120

fix phi 10 -- 3628800