“Lambda-Calculus and Combinators: An Introduction”メモ(その2)
Lemma 1.15
Proof Easy, by checking the clauses of Definition 1.12.
とあるので、実際やってみます。
Lemma 1.15(a)
$\begin{array} &
\mbox{Lemma 1.15(a) } [x/x]M ≡ M \\
\mbox{(1) } M=x \mbox{ の時、つまり definition 1.12 (a)} \\
\mbox{左辺 } [x/x]x ≡ x \\
\mbox{右辺 } x \\
\therefore [x/x]x ≡ x \\
\mbox{(2) } M=a \mbox{ の時 (1.12(b))} \\
\mbox{左辺 } [x/x]a ≡ a \\
\mbox{右辺 } a \\
\therefore [x/x]a ≡ a \\
\mbox{(3) } M=(PQ) \mbox{ の時 (1.12(c))} \\
\mbox{左辺 } [x/x](PQ) ≡ ([x/x]P [x/x]Q) \\
\mbox{ここで帰納法により [n/n]M ≡ M が正しいと仮定して以下を導きます} \\
≡ (PQ) \\
\mbox{右辺 } (PQ) \\
\therefore [x/x](PQ) ≡ (PQ) \\
\mbox{(4) } M=λx.P \mbox{ の時 (1.12(d))} \\
\mbox{左辺 } [x/x](λx.P) ≡ λx.P \\
\mbox{右辺 } λx.P \\
\therefore [x/x](λx.P) ≡ λx.P \\
\mbox{(5) } M=λy.P, \; x \notin FV(P) \mbox{ の時 } (1.12(e)) \\
\mbox{左辺 } [x/x](λy.P) ≡ λy.P \\
\mbox{右辺 } λy.P \\
\therefore [x/x](λy.P) ≡ λy.P \\
\mbox{(6) } M=λy.P, \; x \in FV(P) \mbox{ and } y ≠ x \mbox{ (1.12(f)) では } y \notin FV(N) \mbox{ より} \\
\mbox{左辺 } [x/x](λy.P) ≡ λy.[x/x]P \\
\mbox{ここで帰納法により [n/n]M ≡ M が正しいと仮定して以下を導きます} \\
≡ λy.P \\
\mbox{右辺 } λy.P \\
\therefore [x/x](λy.P) ≡ λy.P \\
\mbox{・1.12(g) について、} \\
\mbox{(g) } [N/x](λy.P) ≡ λz.[N/x][z/y]P, \\
\mbox{if } x \in FV(P) \mbox{ and } y \in FV(N) \\
\mbox{1.12(g)の条件、} y \in FV(N) \mbox{ は } N=x \mbox{ の時に成り立たない} \\
\mbox{なので1.12(g)は考慮しません。} \\
\therefore \mbox{(1) 〜 (6) より [x/x]M ≡ M.}
\end{array}$
Lemma 1.15(b)
$\begin{array} &
\mbox{1.15(b) } x \notin FV(M) \Rightarrow [N/x]M ≡ M \\
\mbox{(1) } M=x \mbox{ の時、つまり definition 1.12 (a) について、} \\
x \notin FV(M) \mbox{ なので、そもそも M=x は成り立たない。} \\
\mbox{(2) } M=a \mbox{ の時 (1.12(b))} \\
\mbox{左辺 } [N/x]a ≡ a \\
\mbox{右辺 } a \\
\therefore [N/x]a ≡ a \\
\mbox{(3) } M=(PQ) \mbox{ の時 (1.12(c))} \\
\mbox{左辺 } [N/x](PQ) ≡ ([N/x]P [N/x]Q) \\
\mbox{ここで帰納法により [N/n]M ≡ M が正しいと仮定して以下を導きます} \\
≡ (PQ) \\
\mbox{右辺 } (PQ) \\
\therefore [N/x](PQ) ≡ (PQ) \\
\mbox{(4) } M=λx.P \mbox{ の時 (1.12(d))} \\
\mbox{左辺 } [N/x](λx.P) ≡ λx.P \\
\mbox{右辺 } λx.P \\
\therefore [N/x](λx.P) ≡ λx.P \\
\mbox{(5) } M=λy.P, \; x \notin FV(P) \mbox{ の時 } (1.12(e)) \\
\mbox{左辺 } [N/x](λy.P) ≡ λy.P \\
\mbox{右辺 } λy.P \\
\therefore [N/x](λy.P) ≡ λy.P \\
\mbox{・1.12(f) について。 } x \notin FV(M) \mbox{ の時、1.12(f)の最初の条件} \\
M=λy.P \mbox{ で } x \in FV(P) \mbox{ が明らかに成り立たない。} \\
\mbox{・1.12(g) についても同様に、} x \in FV(P) \mbox{ が成り立にない。} \\
\therefore \mbox{(1) 〜 (5) より } x \notin FV(M) \Rightarrow [N/x]M ≡ M.
\end{array}$
$1.12(a)$ 成り立たない、という最初が肝心だと思う。
Lemma 1.15(c)
$\begin{array} &
\mbox{1.15(c) } x \in FV(M) \Rightarrow FV([N/x]M) = FV(N) \cup (FV(M) - {x}) \\
\end{array}$
definition 1.12 を照らし合わせます。
$\begin{array} &
\mbox{1.12(a) } M=x \\
\mbox{1.12(b) } M=a \Rightarrow x \in FV(M) \mbox{ が成り立たない} \\
\mbox{1.12(c) } M=(PQ) \\
\mbox{1.12(d) } M=λx.P \Rightarrow x \in FV(M) \mbox{ が成り立たない} \\
\mbox{1.12(e) } M=λy.P \mbox{ if } x \notin FV(P) \Rightarrow x \in FV(M) \mbox{ が成り立たない} \\
\mbox{1.12(f) } M=λy.P \mbox{ if } x \in FV(P) \mbox{ and } y \notin FV(N) \\
\mbox{1.12(g) } M=λy.P \mbox{ if } x \in FV(P) \mbox{ and } y \in FV(N)
\end{array}$
つまり、 Lemma 1.15(c) に当てはまめて substitution しても $M$ に変化が無いものは除外して考えています。
$\begin{array} &
\mbox{(1) } M=x \mbox{ の時 (1.12(a))} \\
\mbox{ (1-1) } N=y \mbox{ の時} \\
\mbox{ 左辺 } FV([y/x]x) = \{y\} \\
\mbox{ 右辺 } FV(y) \cup (FV(x) - \{x\}) = \{y\} \\
\mbox{ (1-2) } N=(PQ) \mbox{ の時} \\
\mbox{ 左辺 } FV([(PQ)/x]x) = FV(PQ) \\
\mbox{ 右辺 } FV(PQ) \cup (FV(x) - \{x\}) = FV(PQ) \\
\mbox{ (1-3) } N=λx.L \mbox{ の時} \\
\mbox{ 左辺 } FV([(λx.L)/x]x) = FV(λx.L) \\
\mbox{ 右辺 } FV(λx.L) \cup (FV(x) - \{x\}) = FV(λx.L) \\
\therefore \mbox{(1) の時、左辺 ≡ 右辺} \\
\mbox{(2) } M=(PQ) \mbox{ の時 (1.12(c))} \\
\mbox{ (2-1) } N=y \mbox{ の時} \\
\mbox{ 左辺 } FV([y/x](PQ)) = FV([y/x]P [y/x]Q) \\
\mbox{ ;; ここで帰納法により } \\
\mbox{ ;; } FV([Y/k]Z) = FV(Y) \cup (FV(Z) - \{k\}) \\
\mbox{ ;; が正しいと仮定して以下を導きます} \\
= (FV(y) \cup (FV(P) - \{x\})) \cup (FV(y) \cup (FV(Q) - \{x\})) \\
= (\{y\} \cup (FV(P) - \{x\})) \cup (\{y\} \cup (FV(Q) - \{x\})) \\
\mbox{ ;; 結合方則で入れ換え} \\
= \{y\} \cup \{y\} \cup (FV(P) - \{x\}) \cup (FV(Q) - \{x\}) \\
\mbox{ ;; 等冪法則} \\
= \{y\} \cup (FV(P) - \{x\}) \cup (FV(Q) - \{x\}) \\
\mbox{ ;; } (A - C) \cup (B - C) = (A \cup B) - C \mbox{ より} \\
= \{y\} \cup ((FV(P) \cup FV(Q)) - \{x\}) \\
= \{y\} \cup (FV(PQ) - \{x\}) \\
\mbox{ 右辺 } FV(y) \cup (FV(PQ) - \{x\}) = \{y\} \cup (FV(PQ) - \{x\}) \\
\mbox{ (2-2) } N=(RS) \mbox{ の時} \\
\mbox{ 左辺 } FV([(RS)/x](PQ)) = FV([(RS)/x]P [(RS)/x]Q) \\
\mbox{ ;; ここで帰納法により、以下を導きます。またこれ以下は (2-1) と同様} \\
= (FV(RS) \cup (FV(P) - \{x\})) \cup (FV(RS) \cup (FV(Q) - \{x\})) \\
= FV(RS) \cup FV(RS) \cup (FV(P) - \{x\}) \cup (FV(Q) - \{x\}) \\
= FV(RS) \cup (FV(P) - \{x\}) \cup (FV(Q) - \{x\}) \\
= FV(RS) \cup ((FV(P) \cup FV(Q)) - \{x\}) \\
= FV(RS) \cup (FV(PQ) - \{x\}) \\
\mbox{ 右辺 } FV(RS) \cup (FV(PQ) - \{x\}) \\
\mbox{ (2-3) } N=λx.L \mbox{ の時} \\
\mbox{ 左辺 } FV([(λx.L)/x]PQ) = FV([(λx.L)/x]P[(λx.L)/x]Q) \\
\mbox{ ;; 以下、 (2-1)・(2-2) と同様} \\
= (FV(λx.L) \cup (FV(P) - \{x\})) \cup (FV(λx.L) \cup (FV(Q) - \{x\})) \\
= FV(λx.L) \cup FV(λx.L) \cup (FV(P) - \{x\}) \cup (FV(Q) - \{x\}) \\
= FV(λx.L) \cup (FV(P) - \{x\}) \cup (FV(Q) - \{x\}) \\
= FV(λx.L) \cup ((FV(P) \cup FV(Q)) - \{x\}) \\
= FV(λx.L) \cup (FV(PQ) - \{x\}) \\
\mbox{ 右辺 } FV(λx.L) \cup (FV(PQ) - \{x\}) \\
\therefore \mbox{(2) の時、左辺 ≡ 右辺} \\
\mbox{(3) } M=y.P, x\in FV(P) \mbox{ and } y \notin FV(N) \mbox{ の時 (1.12(f))} \\
\mbox{ (3-1) } N=z \mbox{ の時} \\
\mbox{ 左辺 } FV([z/x]λy.P) = FV(λy.[z/x]P) = FV([z/x]P - \{y\}) \\
\mbox{ ;; ここで帰納法により } \\
\mbox{ ;; } FV([Y/k]Z) = FV(Y) \cup (FV(Z) - \{k\}) \\
\mbox{ ;; が正しいと仮定して以下を導きます} \\
= FV(z) \cup (FV(P) - \{x\} - \{y\}) \\
= FV(z) \cup (FV(P) - \{x,y\}) \\
= \{z\} \cup (FV(P) - \{x,y\}) \\
\mbox{ 右辺 } FV(z) \cup (FV(λy.P) - \{x\}) \\
= FV(z) \cup (FV(P) - \{x\} - \{y\}) \\
= FV(z) \cup (FV(P) - \{x,y\}) \\
= \{z\} \cup (FV(P) - \{x,y\}) \\
\mbox{ (3-2) } N=(RS) \mbox{ の時} \\
\mbox{ 左辺 } FV([(RS)/x](λy.P)) = FV(λy.[(RS)/x]P) \\
\mbox{ ;; ここで同様に帰納法により、以下を導きます。} \\
= FV(RS) \cup (FV(P) - \{x,y\}) \\
\mbox{ 右辺 } FV(RS) \cup (FV(λy.P) - \{x\}) \\
= FV(RS) \cup (FV(P) - \{x,y\}) \\
\mbox{ (3-3) } N=λx.L \mbox{ の時} \\
\mbox{ 左辺 } FV([(λx.L)/x](λy.P)) = FV(λy.[(λx.L)/x]P) \\
\mbox{ ;; ここで同様に帰納法により、以下を導きます。} \\
= FV(λx.L) \cup (FV(P) - \{x\} - \{y\}) \\
= FV(λx.L) \cup (FV(P) - \{x,y\}) \\
\mbox{ 右辺 } FV(λx.L) \cup (FV(λy.P) - \{x\}) \\
= FV(λx.L) \cup (FV(P) - \{x\} - \{y\}) \\
= FV(λx.L) \cup (FV(P) - \{x,y\}) \\
\therefore \mbox{(3) の時、左辺 ≡ 右辺} \\
\mbox{(4) } M=y.P, x \in FV(P) \mbox{ and } y \in FV(N) \mbox{ の時(1.12(g))} \\
\mbox{ (4-1) } N=y \mbox{ の時} \\
\mbox{ 左辺 } FV([y/x](λy.P)) = FV(λz.[y/x][z/y]P) \\
\mbox{ ;; ここで同様に帰納法により、以下を導きます。} \\
= FV(y) \cup (FV(λz.[z/y]P - \{x\})) \\
= \{y\} \cup (FV(λz.[z/y]P - \{x\})) \\
= \{y\} \cup (FV(λy.P - \{x\})) \\
\mbox{ 右辺 } FV(y) \cup (FV(λy.P) - \{x\}) \\
\mbox{ (4-2) } N=(RS) \mbox{ の時、ただし、} y \in FV(RS) \\
\mbox{ 左辺 } FV([(RS)/x](λy.P)) = FV(λz.[(RS)/x][z/y]P) \\
\mbox{ ;; ここで同様に帰納法により、以下を導きます。} \\
= FV(RS) \cup (FV(λz.[z/y]P - \{x\})) \\
= FV(RS) \cup (FV(λy.P - \{x\})) \\
\mbox{ 右辺 } FV(RS) \cup (FV(λy.P - \{x\})) \\
\mbox{ (4-3) } N=λx.L \mbox{ の時、ただし、} y \in FV(λx.L) \\
\mbox{ 左辺 } FV([(λx.L)/x](λy.P)) = FV(λz.[(λx.L)/x][z/y]P) \\
\mbox{ ;; ここで同様に帰納法により、以下を導きます。} \\
= FV(λx.L) \cup (FV(λz.[z/y]P - \{x\})) \\
= FV(λx.L) \cup (FV(λy.P - \{x\})) \\
\mbox{ 右辺 } FV(λx.L) \cup (FV(λy.P - \{x\})) \\
\therefore \mbox{(4) の時、左辺 ≡ 右辺} \\
\therefore \mbox{(1) 〜 (4) より }
x \in FV(M) \Rightarrow FV([N/x]M) = FV(N) \cup (FV(M) - {x}). \\
\end{array}$
Lemma 1.15(d)
$\begin{array} &
\mbox{1.15(d) } lgh([y/x]M) = lgh(M)
\end{array}$
$\begin{array} &
\mbox{(1) } M=x \mbox{ の時 (1.12(a))} \\
\mbox{ 左辺 } lgh([y/x]x) = lgh(y) = 1 \\
\mbox{ 右辺 } lgh(x) = 1 \\
\therefore \mbox{(1) の時、左辺 ≡ 右辺} \\
\mbox{(2) } M=a \mbox{ の時 (1.12(b))} \\
\mbox{ 左辺 } lgh([y/x]a) = lgh(a) = 1 \\
\mbox{ 右辺 } lgh(a) = 1 \\
\therefore \mbox{(2) の時、左辺 ≡ 右辺} \\
\mbox{(3) } M=(PQ) \mbox{ の時 (1.12(c))} \\
\mbox{ 左辺 } lgh([y/x](PQ)) \\
= lgh([y/x]P [y/x]Q) = lgh([y/x]P) + lgh([y/x]Q) \\
\mbox{ ;; ここで帰納法により } \\
\mbox{ ;; } lgh([l/k]Z) = lgh(Z) \\
\mbox{ ;; が正しいと仮定して以下を導きます} \\
= lgh(P) + lgh(Q) \\
\mbox{ 右辺 } lgh(PQ) = lgh(P) + lgh(Q) \\
\therefore \mbox{(3) の時、左辺 ≡ 右辺} \\
\mbox{(4) } M=λx.P \mbox{ の時 (1.12(d))} \\
\mbox{ 左辺 } lgh([y/x](λx.P)) = lgh(λx.P) \\
\mbox{ 右辺 } lgh(λx.P) \\
\therefore \mbox{(4) の時、左辺 ≡ 右辺} \\
\mbox{(5) } M=λy.P \mbox{ if } x \notin FV(P) \mbox{ の時 (1.12(e))} \\
\mbox{ 左辺 } lgh([y/x](λy.P)) = lgh(λy.P) \\
\mbox{ 右辺 } lgh(λy.P) \\
\therefore \mbox{(5) の時、左辺 ≡ 右辺} \\
\mbox{(6) } M=λy.P \mbox{ if } x \in FV(P) \mbox{ and } y \notin FV(N) \mbox{ の時 (1.12(f))} \\
FV(N) \Rightarrow \{y\} \mbox{ すなわち } y \in FV(N) \mbox{ だから成り立たない} \\
\mbox{(7) } M=λy.P \mbox{ if } x \in FV(P) \mbox{ and } y \in FV(N) \mbox{ の時 (1.12(g))} \\
\mbox{ 左辺 } lgh([y/x](λy.P)) = lgh(λz.[y/x][z/y]P) = 1 + lgh([y/x][z/y]P) \\
\mbox{ ;; ここで帰納法により } \\
\mbox{ ;; } lgh([l/k]Z) = lgh(Z) \\
\mbox{ ;; が正しいと仮定して以下を導きます} \\
= 1 + lgh(P) \\
\mbox{ 右辺 } lgh(λy.P) = 1 + lgh(P) \\
\therefore \mbox{(7) の時、左辺 ≡ 右辺} \\
\mbox{(6)' } M=λz.P \mbox{ if } x \in FV(P) \mbox{ and } z \notin FV(N) \mbox{ の時 (1.12(f))} \\
\mbox{ 左辺 } lgh([y/x](λz.P)) = lgh(λz.[y/x]P) = 1 + lgh([y/x]P) \\
\mbox{ ;; ここで帰納法により } \\
\mbox{ ;; } lgh([l/k]Z) = lgh(Z) \\
\mbox{ ;; が正しいと仮定して以下を導きます} \\
= 1 + lgh(P) \\
\mbox{ 右辺 } lgh(λz.P) = 1 + lgh(P) \\
\therefore \mbox{(6)' の時、左辺 ≡ 右辺} \\
\mbox{(7)' } M=λz.P \mbox{ if } x \in FV(P) \mbox{ and } z \in FV(N) \mbox{ の時 (1.12(g))} \\
FV(N) \Rightarrow \{y\} \mbox{ すなわち } z \notin FV(N) \mbox{ だから成り立たない} \\
\therefore \mbox{(1) 〜 (7)' より } lgh([y/x]M) = lgh(M).
\end{array}$
$1.12(g)$ が成り立つ、成り立たない場合を両方考えます。