“Lambda-Calculus and Combinators: An Introduction”メモ(その6)
Lemma A1.8
$x,y$ を bound させて α0-contraction と α-contraction とのギャップを埋めている、ということだろうか。
Every α-contraction can be done by a series of α0-contractions.
A1.7 の $M^\prime$ を取り出して、$λx.M \rhd_{\alpha0} λx.M^\prime$ と言っています。これは、 A1.7 の条件の $M,M^\prime$ から今度は $λx.M$ を考えた時、 $λx.M \rhd_{\alpha0} λx.M^\prime$ が成り立つのは明らかです。これを部分式として考えると $x,y$ が bound なので α-contraction の条件と重なることになります。
$\begin{array} &
λx.M & \rhd_{\alpha0} & λx.M^\prime \\
λx.M^\prime & \rhd_{1\alpha0} & λy.[y/x]M^\prime \\
\mbox{ ここで} \\
λx.M & \rhd_{1\alpha0} & λy.[y/x]M \\
\mbox{ より} \\
λy.[y/x]M^\prime & \rhd_{\alpha0} & λy.[y/x]M.
\end{array}$