不動点演算子の使い方

ねたに困ったときはライトな?話題でも。いつもどおりだらだらと。
λ計算にて再帰的な関数の意味づけに不動点演算子というものを用いる。
不動点演算子(Y)は、λ式Mに対して

Y M = M (Y M)

を満たすようなλ式で、
具体的には

Y = λf.(λx.f(x x)) (λx.f(x x))

と定義される(これは一例。定義は他にも考えられる)。
数学的には(Y M)がMの不動点になっているので、
Yを不動点演算子というのだが、

Y M => M (Y M) => M (M (Y M)) => ...

のようにMを繰り返し適用できるので再帰的な計算を行える。
ここでYの型を考えると、Y MがMの不動点なので

Y :: (a -> a) -> a

このようになる。
ちなみに上で定義したλ式をHaskellでそのまま入力すると
型が付けられないのでエラーとなる。
(型付λ計算にて不動点演算子は定義出来ない…?
手持ちの資料ではプリミティブに与えられることになっている)
letを用いると

y :: (a -> a) -> a
y m = let v = m v in v

このように定義することが出来る。
しかし実はこれ、不動点演算子はControl.Monad.Fixにfixという
名前の関数として用意されている。

このようなものを使うと何が嬉しいのか?
それは変数定義を使わずに再帰関数を作り出せることだろう。
そういうことが出来ると関数に関数を渡すときなど、
気軽に再帰関数をその場で作って渡すことが出来る。
たとえば、再帰的に定義されたfactorial、

fact n = if n==0 then 1 else n*fact (n-1)

このような関数をλ式のみで記述しようと思うと結構大変である。
(実際のところ不動点演算子を自分で作るような感じになるとは思うのだが)
ここでfixを用いると、(やや天下り的ではあるが…)

fact = fix $ \f n -> if n==0 then 1 else n*f (n-1)

このように定義できる。
この関数の動作は全く自明ではない(と思う…)ので、
なぜこれで正しいのか見ていくことにする。

とりあえず、

\f n -> if n==0 then 1 else n*f (n-1)

これをMと置くと、

fix M = M (fix M) = ... = M (M (M ... (fix M) ...))

fix M はこのように簡約できるのであるが、
実際のところ遅延評価によりこの計算は有限で終わらせることが出来る。
factの使用時には後ろに数字を渡すので、
実際に簡約されるのは

fix M 10

のような式である。これを計算すると、

fix M 10
=> M (fix M) 10 => (fix M を M (fix M) に)
=> 10 * ( (fix M) (10-1)) (Mを簡約)

ここで fix M 9 が現れている。
なんだかいけそうな感じがしてきたが、途中をすっ飛ばして
最後のほうも計算してみる。

10*...*1*( (fix M) (1-1))
=> 10*...*1*(M (fix M) (1-1))
=> 10*...*1*1 (n==0なので1に簡約される)
=> 3628800

ということで確かに計算が終わる。

このようにfactが作れることはわかったが、
他のもの等はどのようにつくればいいのだろうか。
Mを適当な式として、
fix M = M (fix M) なのであるから、Mの第一引数にはfix Mが渡される。
先の例ではこれをfactと置いていたので、まさにこれが渡されるということになる。
ということはこれを呼び出すと再帰的呼び出しが出来るのである。

形式的に考えると、

\f n -> if n==0 then 1 else n*f (n-1)

これは

fact n = if n==0 then 1 else n*fact (n-1)

これと酷似している。
上の式ではfに自分自身が渡されると考えてもさして
差支えが無さそうである。

他の関数も考えてみる。

ones = 1:ones

これは単なる1の無限リストであるが、
先と同様に

fix $ \ones -> 1:ones

このように書くことが出来る。

take 10 $ fix $ \ones -> 1:ones
=> [1,1,1,1,1,1,1,1,1,1]

2引数のもの、

gcd a b = if a `mod` b == 0 then b else gcd b (a `mod` b)

たとえばこのようなものも

fix $ \gcd a b -> if a `mod` b == 0 then b else gcd b (a `mod` b)

同じように形式的に変換できる。

(fix $ \gcd a b -> if a `mod` b == 0 then b else gcd b (a `mod` b)) 12 8
=> 4

最初の方に戻って、これらのことの不動点的な意味を考えてみる…

m = \f n -> if n==0 then 1 else n*f (n-1)

これの型は(Int -> Int) -> (Int -> Int)
つまり関数が渡されると関数が返る。
fix m :: Int -> Int が m の不動点であるという話である。
ということは fact = fix m にてm fact = factが成り立つということで、
結局fに渡される関数fix fはfに渡されるたびに変化しないもの、
常に同じものが渡されることになり、これにより確かに再帰的な
計算が行えるのである(…?なんか日本語がよく分からんことになってしまった)。

…分かったような分からんような内容になったが、
まぁ、使えりゃ問題なし。ということで。