“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$ で、成り立たないのがわかる。