不動点が複数の関数である関数の例
/mrsekut-book-4320026578/088の\Phi_{\mathrm{fact}^\circ}の例を見る
この関数は、無限個の不動点を持つ
Haskellで書くと
この関数
fact' を元にした高階関数 phi' を考えるhsfact' x = if x == 10 then fact 10 else x * fact' (x-1) hsphi' f x = if x == 10 then fact 10 else x * f (x-1)ちなみに、式内の
fact は、通常の階乗関数 fact この
phi' には複数の不動点が存在する全ての不動点
g は以下の形で表せるg_\alpha(x)= \begin{cases}x ! * \alpha & (0 \leqq x<10) \\ x ! & (10 \leqq x)\end{cases}
ここで、\alphaは、
undefined または任意の自然数\alphaは無限個あるので、
phi' の不動点も無限個あるといえる例えば、
α = undefined の時hsg_ x
| x < 10 = undefined
| otherwise = fact xこの
g_ は確かに、 phi' g_ と等しい挙動になるだから
g_ は phi' の不動点であるこれは
fact' と表示的意味論的には同じなので、 g_ = fact' fact' の方は、 undefiend ではなく無限ループになるけど、無限ループを undefiend に表すなら同じになる例えば、
α = 2 の時hsg2 x
| x < 10 = fact x * 2
| otherwise = fact xこの
g2 は確かに、 phi' g2 と等しい挙動になるだから
g2 は phi' の不動点である部分関数における意味近似順序の観点で見れば、
g2 の方が、 g_ よりも多く定義されている関数になので、g_\bot \sqsubset g_2という関係になる
平坦領域になるはず
だから、
fix phi' の返り値は g_ に等しくなるちなみに、不動点が複数の値である関数の例は、
id とか任意の値が不動点
(*3) とか 0 、 undefined など