■
計算論のP.66のβ変換における等号表現である
を定義する時に現れる表現
の定義なんだけど、直感的に
と思ってたけど
なんだね
不動点演算子Yの定義で、Mの不動点演算子Yに対して
YM -> M'(M' ≡ M''M'', M'' ≡ λx. M(xx) ) からいきなり YM = M'を導いてたから悩んだ
要するに
M -> P1 -> P2 -> ... -> P_s <- .... <- N を満たすλ式 P1,P2,...が存在するならば M = Nと。
※ ->をβ変換、=をβ等号の意味で書いた。また以下では ->>をβ変換列の意味として書く
[問2.1.5] Y' ≡ XX, X ≡ λxy. y(xxy)の時 Y'M ->> M(Y'M)となることを証明せよ [証明] 定義より Y'M ≡ XXM -> (λxy. y(xxy))XM -> (λy. y(XXy))M -> M(XXM) ≡ M(Y'M) よって Y'M ->> M(Y'M) □