Zコンビネータ
Y = (λf. (λx. f (x x)) (λx. f (x x))) 代わりにZコンビネータを使うと、正格評価においても不動点コンビネータとして機能する
Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y)) h h とかfctとかが遠回りだ
あー、もしかしてちゃんと正格評価するとこうなのか？
そういうことだった
ググると、以下の記事が上位にヒットするが、簡約の計算の最後でどちらも同じ間違いをしている
正しくは
Aa = M(\y.Ay)a であり、最後の変形はできないM(\y.Ay)aは、(M(\y.Ay))aであって、右側の二項を結合できない
正しくは
(g (\y. (z g) y)) n であり、最後の変形はできない左結合のところを間違って右結合してる
x y z は(x y) zであり、関数適用に結合法則は無いので、(x y) z ≠ x (y z)
簡約という変形は、数学的な式変形とは違うということも注意しないといけない
簡約ではなく、式変形のような形で説明すると
fZ := λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
このとき
Z f = (λx. f (λy. x x y)) (λx. f (λy. x x y) //①
= f (λy. (λx. f (λy. x x y) (λx. f (λy. x x y) y)
================== ================== ここが①と同じ
= f (λy. Z f y)
= f (λy. Z f y)
なにか引数を渡したとしても
Z g n
= g (λy. Z g y) n変形できるのはここまでである
(λy. Z g y) が、 Z g の遅延評価に相当する下線部をZ fにするところが、簡約でない箇所であり、厳密性には欠ける