■ - ウォンツテック

　計算論のP.66のβ変換における等号表現である
$M \underset{\beta}{=} N$
を定義する時に現れる表現
$M \underset{\beta}{\leftrightarrow} N$
　の定義なんだけど、直感的に
$M \underset{\beta}{\to} N and N \underset{\beta}{\to} M$
と思ってたけど
$M \underset{\beta}{\to} N or N \underset{\beta}{\to} M$
なんだね

不動点演算子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) □