Yコンビネータ
$ Y\equivλf.(λx.f (x x)) (λx.f (x x))
無名関数で再帰を行っている
任意のラムダ抽象$ Mに対して以下が成り立つ
$ YM=_\beta M(YM)
証明
code:_
YM = λf.(λx.f(xx))(λx.f(xx))M
= (λx.M(xx))(λx.M(xx)) -- ①
= M(λx.M(xx)(λx.M(xx)))
= M (YM) -- ∵ ①
参考
SKIからYを作る
Yコンビネータの引数に関数Mを与える
Y M = M (M (M (M ...)))というイメージ
YM = M(YM)の意味
MにYMを適用した結果は、M(YM)だが、これがYMに等しい
というのを繰り返すと
YM = M(YM)
YM = M(M(YM))
YM = M(M(M(M(M(M(...(YM)...))))
となる
YMにMを何回適用してもYMになる
関数にその関数自身を適用させるときにYを適用させておくと、そのまま同じものが帰ってくるので、Yを不動点演算子といいます。
hs
$ Y\equivλf·(λx·f (x x)) (λx·f (x x))
x xの部分がミソ
これは型なし言語だからこそできる記述
最初のxは適用するものだが、二番目のxは適用されるもの
なので、x同士で型が異なり、型が定まらない
Haskell