Yコンビネータ
Y\equivλf.(λx.f (x x)) (λx.f (x x))
無名関数で再帰を行っている
任意のラムダ抽象Mに対して以下が成り立つ
YM=_\beta M(YM)
証明
_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