“Combinatory Logic Volume I”メモ(その2)
p.98 のメモ、最後の remark のところ。
おさらいで、 $(c)$
$\begin{array} &
N' ≡ [M/x]N \\
[M/x][N/y]X ≡ [N'/y][M/x]X
\end{array}$
条件は以下です。
(c) If no variables which occur free in M or N are bound in X,
$\begin{array} &
X ≡ λx.fxy \\
M ≡ a \mbox{ ;; a variable not otherwise used), } \\
N ≡ x. \\
\\
\begin{array}{ll}
N' &≡ [M/x]N \\
&≡ [a/x]x \\
&≡ a \\
X\ast &≡ [M/x][N/y]X \\
&≡ [a/x][x/y]λx.fxy \\
&≡ [a/x]λz.fzx \\
&≡ λz.fza \\
X\# &≡ [N'/y][M/x]X \\
&≡ [N'/y][a/x]λx.fxy \\
&≡ [N'/y]λx.fxy \\
&≡ [a/y]λx.fxy \\
&≡ λx.fxa \\
\end{array} \\
\end{array}$
$x$ occurs free in $N$ で、成り立たないのがわかる。