不動点が複数の関数である関数の例

/mrsekut-book-4320026578/088の$ \Phi_{\mathrm{fact}^\circ}の例を見る

この関数は、無限個の不動点を持つ

Haskellで書くと

この関数fact'を元にした高階関数phi'を考える

code:hs

fact' x = if x == 10 then fact 10 else x * fact' (x-1)

code:hs

phi' f x = if x == 10 then fact 10 else x * f (x-1)

ちなみに、式内のfactは、通常の階乗関数factmrsekut.icon

このphi'には複数の不動点が存在する

全ての不動点gは以下の形で表せる

$ g_\alpha(x)= \begin{cases}x ! * \alpha & (0 \leqq x<10) \\ x ! & (10 \leqq x)\end{cases}

ここで、$ \alphaは、undefinedまたは任意の自然数

$ \alphaは無限個あるので、phi'の不動点も無限個あるといえる

例えば、α = undefinedの時

code:hs

g_ x

| x < 10 = undefined

| otherwise = fact x

このg_は確かに、phi' g_と等しい挙動になる

だからg_はphi'の不動点である

これはfact'と表示的意味論的には同じなので、g_ = fact'

fact'の方は、undefiendではなく無限ループになるけど、無限ループをundefiendに表すなら同じになるmrsekut.icon

例えば、α = 2の時

code:hs

g2 x

| x < 10 = fact x * 2

| otherwise = fact x

このg2は確かに、phi' g2と等しい挙動になる

だからg2はphi'の不動点である

部分関数における意味近似順序の観点で見れば、

g2の方が、g_よりも多く定義されている関数になので、

$ g_\bot \sqsubset g_2という関係になる

平坦領域になるはずmrsekut.icon

だから、fix phi'の返り値はg_に等しくなる

idとか

任意の値が不動点

(*3)とか

0、undefinedなど