Zコンビネータ

Y = (λf. (λx. f (x x)) (λx. f (x x)))

Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

h h とかfctとかが遠回りだ

あー、もしかしてちゃんと正格評価するとこうなのか？

そういうことだった

ググると、以下の記事が上位にヒットするが、簡約の計算の最後でどちらも同じ間違いをしている

https://gyazo.com/7470631d8d8cc8711e71c29e1778b48c

M(\y.Ay)aは、(M(\y.Ay))aであって、右側の二項を結合できない

https://gyazo.com/56896f8f64c0a945fab6bf208c56cf21

左結合のところを間違って右結合してる

x y z は(x y) zであり、関数適用に結合法則は無いので、(x y) z ≠ x (y z)

簡約という変形は、数学的な式変形とは違うということも注意しないといけない

簡約ではなく、式変形のような形で説明すると

code:f

Z := λ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

変形できるのはここまでである

下線部をZ fにするところが、簡約でない箇所であり、厳密性には欠ける