fix関数に適用したら無限ループになる理由 - mrsekut-p

fix関数に適用したら無限ループになる理由

前提

不動点コンビネータであるfix関数は、引数に取った関数fの最小不動点を返す

関数fの不動点とは、f x == xを満たすxのことである

この等式を満たすxは複数存在することもある

fixはその内の最小なものを返す

以下の疑問に答える

関数f = (*3)をfixに適用した時に、なぜ0じゃなくて無限ループになるのか？

code:ghci(hs)

f = (*3) -- f :: Int -> Int

fix f -- 無限ループ！

「最小」と言うのだから、0 * 3 == 0なんだし0が返ってくるべきでは？と思ったりする

「最小」とは言うが、何の順序の話をしているのかを捉え違えるとこう誤解するmrsekut.icon

その順序がIntの数値の大小関係$ \leの話ならば確かに0かもしれない

しかし、ここでの順序はそれではない

結論

ここでの順序関係は、意味近似順序のことである

最小不動点は、この順序における最小なものを返す

それがf = (*3)の場合は、undefinedなので無限ループになる

以下のことを抑えておく必要がある

undefinedの表す意味

未定義

無限ループ

$ \mathrm{Int}_\botにおける意味近似順序

例えば、以下の関数を考える

code:hs

f = const "x"

これは、引数に何を取っても"x"を返す関数

code:hs

f 1 -- "x"

f True -- "x"

f "x" -- "x"

..

このfの不動点は唯一つであり、それは"x"

従って、最小不動点は"x"である

実際、fix fの返り値は"x"になる

これは不動点の例として直観に沿う簡単な例mrsekut.icon

例えば、以下の関数を考える

code:hs

f = (*3)

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

例えば、0

∵ 0 * 3 == 0

例えば、undefined

∵ undefined * 3 == undefined

この時、どちらがより小さいか？が問題になる

以下2点を抑える必要がある

どういう集合を考えているのか？

ここで考えている集合は、Haskellの型Intである

Haskellの型は常に通常の0引数の型にbottom(⊥)を加えた集合になることに注意する

つまり、Int = {...,-1,0,1,...} ∪ {undefiend}である

どういう順序を考えているのか？

ここで考えている順序は、意味近似順序である

この2点を踏まえるとIntの意味近似順序を表したハッセ図式は以下のようになる

https://gyazo.com/69376315a7ae1032b1a9a6fd3506f859

任意の整数$ nに対して、$ \mathrm{undefined} \sqsubset nだし、

0や1の間には順序は定義されていない

ここで、元のfの不動点は0とundefinedがあった

この時、順序関係は$ \mathrm{undefined} \sqsubset 0である

故に、最小不動点はundefined

実際、fix fの返り値は、無限ループになる

結論

不動点が複数あり、その中に$ \botを含む場合はfixによって$ \botが得られる

この$ \botには、未定義や無限ループが含まれる