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
β→ f ((λyx. y (x y x)) f (λyx. y (x y x)))
β→ f ((λx. f (x f x)) (λyx. y (x y x)))
β→ 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を内包して増加増幅していきます。
β→ (λ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とすると、
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
β→ 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'
みたいな感じに増えていきます。
とすると、
A f ≡ fA' ≡ ffA' ≡ fffA'
みたいな感じに増えていきます。
違いというか、簡約された結果だけ見ると、全部同じですね。
与えられたラムダ式fを内包して増加増幅していきます。