“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$ で、成り立たないのがわかる。
“Combinatory Logic Volume I”メモ(その2)
p.98 のメモ、$(c_2)$ の (5) のところ。 もともとの $(c_2)$ の前提は以下:
$(c_2) \mbox{ x does not occur free in X }$
$(c)$ から書くと
$\begin{array} &
\begin{array}{llll}
(c) & [M/x][N/y]X &≡ [N'/y][M/x]X & \mbox{ ;; (b) より } \\
& [M/x][N/y]X &≡ [N'/y]X.
\end{array}
\end{array}$
This statement is trivial if …
まず前半:
if $y$ does not occur in $X$
$\begin{array} &
\begin{array}{lll}
X\ast &≡ [M/x]X. & \mbox{ ;; (b) より } \\
&≡ X. & \mbox{ ;; } (c_2) \mbox{ の前提より } \\
X\# &≡ [M/x]X. & \mbox{ ;; (b) より } \\
&≡ X. & \mbox{ ;; } (c_2) \mbox{ の前提より } \\
\end{array} \\
\therefore X\ast ≡ X\#.
\end{array}$
つづいて後半:
if $x$ does not occur in $N$
$\begin{array} &
\begin{array}{lll}
N' &≡ [M/x]N & \mbox{ ;; なので ( (c) より) } \\
&≡ N & \mbox{ ;; 前提より } \\
\end{array} \\
\mbox{ ;; Case 1 (a) は } (c_2) \mbox{ の前提によりなりたたない} \\
\mbox{ ;; Case 1 (b) } X ≡ y ≠ x \\
\begin{array}{lll}
X\ast &≡ [M/x][N/y]y & \\
&≡ [M/x]N & \mbox{ ;; 前提より } \\
&≡ N & \\
X\# &≡ [N/y]y & \\
&≡ N &
\end{array} \\
\therefore X\ast ≡ X\#. \\
\\
\mbox{ ;; Case 2 } \\
\mbox{ 帰納法により } \\
X\ast ≡ X\astY\ast ≡ X\#Y\# ≡ X\# \\
\therefore X\ast ≡ X\#.
\\
\mbox{ ;; Case 3 (a)} \\
X ≡ λzY \mbox{ と置く } \\
\mbox { ;; 前提より (x does not occur in N) から z ≡ x が成り立つ} \\
\begin{array}{lll}
X\ast &≡ [M/x][N/y]λxY & \\
&≡ [M/x]λx.[N/y]Y & \\
&≡ λx.[N/y]Y & \\
X\# &≡ [N/y]λxY & \\
&≡ λx.[N/y]Y & \\
\end{array} \\
\\
\mbox { ;; Case 3 (a)} \\
X ≡ λzY \mbox{ と置く } \\
\mbox { ;; 前提より } (c_2) \mbox{ z ≡ y が成り立つ} \\
\begin{array}{lll}
X\ast &≡ [M/x][N/y]λyY & \\
&≡ [M/x]λyY & \\
&≡ λy.[M/x]Y & \mbox{ ;; 前提より } (c_2) \\
&& \mbox{ x does not occur free in X }\\
&& (X ≡ λyY) \\
&≡ λyY & \\
X\# &≡ [N/y]λyY & \\
&≡ λyY & \\
\end{array} \\
\therefore X\ast ≡ X\#. \\
\\
\mbox { ;; Case 3 (b)} \\
\mbox { ;; もともとの前提より } \\
\mbox { ;; (c) If no variables which occur free in M or N are boun in X } \\
\mbox { ;; z ≠ x, z ≠ y なので、 成り立たない} \\
\\
\end{array}$
“Combinatory Logic Volume I”メモ(その1)
p.98 のメモ、$(c_1)$ の Case 3のところ。
まず、 “first trivial case” と “second” について。
もともとの前提から:
$\mbox{ (c) If no variables which occur free in M or N are bound in X }$
この前提から導くことを考えます。
$\begin{array} &
X ≡ λz.Y \mbox{ と置く}
\end{array}$
$\begin{array} &
\mbox{ z ≡ y の時} & & \\
\begin{array}{lll}
X\ast &≡ [M/x][N/y]λz.Y & \mbox{ ;; ここで } z ≡ y \mbox{ なので} \\
&≡ [M/x][N/y]λy.Y & \mbox{ ;; Case 3 (a) より} \\
&≡ [M/x]λy.Y & \mbox{ ;; ここでもともとの前提 (c) から} \\
&& \mbox{ ;; y is not free in M なので Case 3 (b) (i) より} \\
&≡ λy.[M/x]Y \\
X\# &≡ [N'/y][M/x]λz.Y & \mbox{ ;; ここで } z ≡ y \mbox{ なので} \\
&≡ [N'/y][M/x]λy.Y & \mbox{ ;; ここで同様にもともとの前提 (c) から} \\
&& \mbox{ ;; y is not free in M なので Case 3 (b) (i) より} \\
&≡ [N'/y]λy.[M/x]Y & \mbox{ ;; Case 3 (a) より} \\
&≡ λy.[M/x]Y \\
\end{array} \\
\therefore X\ast ≡ X\#.
\end{array}$
$\begin{array} &
\mbox{ z ≡ x の時} \\
\begin{array}{lll}
X\ast &≡ [M/x][N/y]λz.Y & \mbox{ ;; ここで } z ≡ x \mbox{ なので} \\
&≡ [M/x][N/y]λx.Y & \mbox{ ;; ここでもともとの前提 (c) から} \\
&& \mbox{ x is not free in N なので Case 3 (b) (i) より} \\
&≡ [M/x]λx.[N/y]Y & \mbox{ ;; Case 3 (a) より} \\
&≡ λx.[N/y]Y \\
X\# &≡ [N'/y][M/x]λz.Y & \mbox{ ;; ここで } z ≡ x \mbox{ なので} \\
&≡ [N'/y][M/x]λx.Y & \mbox{ ;; Case 3 (a) より} \\
&≡ [N'/y]λx.Y & \mbox{ ;; N' について N であらわすと} \\
&≡ [([M/x]N)/y]λx.Y & \mbox{ ;; ここでもともとの前提 (c) から}\\
&& \mbox{ x is not free in N なので [M/x]N ≡ N より} \\
&≡ [N/y]λx.Y & \mbox{ ;; ここで同様にもともとの前提 (c) から} \\
&& \mbox{ x is not free in N なので Case 3 (b) (i) より} \\
&≡ λx.[N/y]Y \\
\end{array} \\
\therefore X\ast ≡ X\#.
\end{array}$