ラムダ計算のYの使い方と不動点コンビネータの違い

1.YCombinatorの使い方

ハスケルのYコンビネータ
Y　≡　(λg. (λx. g(x x)) (λx. g(x x)))

は以下のように簡約されていき、

β→  (λg. (λx. g(x x)) (λx. g(x x))) f

β→  (λx. f(x x)) (λx. f(x x)))

β→  f((λx. f(x x)) (λx. f(x x))))

β→  f(f((λx. f(x x)) (λx. f(x x)))))

で、
Y' ≡(λx. f(x x)) (λx. f(x x))
とすると、
Yf ≡ fY' ≡ ffY' ≡ fffY'
みたいな感じに増えていきます。

引数として与える関数fは、
f = λhy. if condition? then <終了時の処理など> else <再帰呼び出しなど>
のようにして書きます。

・この時、f = h(つまり、再帰呼び出し的な自分自身)だと考える。
・上のラムダ抽象の変数yは、ラムダ抽象が表す関数の引数だと考える。

再帰呼出風に書くとちゃんとループになるというわけです。

Yコンビネータは、Yf ≡ fY' ≡ ffY' ≡ fffY'みたいに増えてい来ます。
しかし、fが表すラムダ抽象は、引数をあたえられた時のβ簡約において、
hを展開させないようにすることで、fffY'のY'を切り捨てます。
結果、ループが止まります。

2.他の不動点コンビネータ

ちなみに、
A ≡(λxy. x y x) (λyx. y (x y x))

このコンビネータは、

β→  (λxy. x y x) (λyx. y (x y x)) f
β→  (λy. (λyx. y (x y x)) y (λyx. y (x y x))) f

β→  (λyx. y (x y x)) f (λyx. y (x y x))

β→  (λx. f (x f x)) (λyx. y (x y x))
β→  f ((λyx. y (x y x)) f (λyx. y (x y x)))
β→  f ((λx. f (x f x)) (λyx. y (x y x)))

β→  f (f ((λyx. y (x y x)) f (λyx. y (x y x))))

でやっぱり、

A' ≡(λyx. y (x y x)) f (λyx. y (x y x))
とすると、
A f ≡ fA' ≡ ffA' ≡ fffA'
みたいな感じに増えていきます。

Θ ≡ (λxy. y(x x y)) (λxy. y(x x y))
これは、「チューリングの不動点コンビネータ」と呼ぶようです。

β→  (λxy. y(x x y)) (λxy. y(x x y)) f

β→  (λy. y((λxy. y(x x y)) (λxy. y(x x y)) y)) f
β→  f ((λxy. y(x x y)) (λxy. y(x x y)) f)
β→  f ((λy. y((λxy. y(x x y) (λxy. y(x x y) y)) f)

β→  f ( f((λxy. y(x x y) (λxy. y(x x y) f)

でやっぱり、

A' ≡((λxy. y(x x y)) (λxy. y(x x y)) f)
とすると、
A f ≡ fA' ≡ ffA' ≡ fffA'
みたいな感じに増えていきます。

違いというか、簡約された結果だけ見ると、全部同じですね。
与えられたラムダ式fを内包して増加増幅していきます。

参考文献

• 主要なコンビネータのまとめと、チャーチエンコーディングのまとめとか : http://jwodder.freeshell.org/lambda.html