“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}$

“Lambda-Calculus and Combinators: An Introduction”メモ(その5)

Lemma A1.7

$\begin{array} & \mbox{For all } M, x \mbox{ and } y \notin FV(xM), \mbox{there exists } M^\prime \mbox{ such that } \\ y \mbox{ is neither free nor bound in } M^\prime \mbox{ and } x \mbox{ is not bound in } M^\prime \mbox{, and } \\ M \rhd_{\alpha0} M^\prime, \qquad [y/x]M \rhd_{\alpha0} [y/x]M^\prime \end{array}$

$M$ の構造的帰納法で証明します。

$(1) M ≡ x$ の時

$\begin{array} & M ≡ x \mbox{ の時 } M^\prime ≡ x \\ \mbox{ここで } [y/x]M ≡ y \mbox{, } [y/x]M^\prime ≡ y \mbox{ なので } [y/x]M ≡ [y/x]M^\prime \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$(2) M ≡ y$ の時

$\begin{array} & M ≡ y \mbox{ の時 } M^\prime ≡ y \\ \mbox{ここで } [y/x]M ≡ y \mbox{, } [y/x]M^\prime ≡ y \mbox{ なので } [y/x]M ≡ [y/x]M^\prime \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$(3) M ≡ a$ の時

$\begin{array} & M ≡ a \mbox{ の時 } M^\prime ≡ a \\ \mbox{ここで } [y/x]M ≡ a \mbox{, } [y/x]M^\prime ≡ a \mbox{ なので } [y/x]M ≡ [y/x]M^\prime \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$(4) M ≡ λx.L$ の時

$\begin{array} & M^\prime ≡ λa.[a/x]L \mbox{ ;; } a \notin FV(L) \\ [y/x]M ≡ [y/x]λx.L ≡ λx.L ~ \cdots (A)\\ [y/x]M^\prime ≡ [y/x]λa.[a/x]L ≡ λa.[y/x][a/x]L \\ \mbox{;; Lemma1.16(e) より } \\ ≡ λa.[([y/x]a)/x]L ≡ λa.[a/x]L ~ \cdots (B) \\ \mbox{帰納法により } L^\prime \rhd_{\alpha0} [a^\prime/x^\prime]L^\prime \\ \mbox{が正しいと仮定して以下を導きます} \\ \mbox{(A), (B) は定義から } λx.L \rhd_{\alpha0} λa.[a/x]L \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$(5) M ≡ λy.L$ の時

$\begin{array} & M^\prime ≡ λa.[a/y]L, ~ a \notin FV(L) \\ [y/x]M ≡ [y/x]λy.L ≡ λz.[y/x][z/y]L \\ \mbox{;; Lemma1.16(c) より } \\ \mbox{;; } [P/x][Q/y]M ≡ [([P/x]Q)/y][P/x]M, ~ y \notin FV(P) \\ ≡ λz.[([y/x]z)/y][y/x]L ≡ λz.[z/y][y/x]L \\ \mbox{;; Lemma1.16(a) より } \\ \mbox{;; } [P/v][v/x]M ≡ [P/x]M, ~ v \notin FV(M) \\ \mbox{;; 条件 } y \notin FV(xM) \mbox{ より} \\ ≡ λz.[z/x]L ~ \cdots (A) \\ [y/x]M^\prime ≡ [y/x]λa.[a/y]L ≡ λa.[y/x][a/y]L \\ \mbox{;; 同様に Lemma1.16(c) より} \\ ≡ λa.[([y/x]a)/y][y/x]L ≡ λa.[a/y][y/x]L \\ \mbox{;; 同様に Lemma1.16(a) より } \\ ≡ λa.[a/x]L ~ \cdots (B) \\ \mbox{帰納法により } [z^\prime/x^\prime]L^\prime \rhd_{\alpha0} [a^\prime/x^\prime]L^\prime \\ \mbox{が正しいと仮定して以下を導きます} \\ \mbox{(A),(B) より } λz.[z/x]L \rhd_{\alpha0} λa.[a/x]L \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$(6) M ≡ λa.L$ の時

$\begin{array} & M^\prime ≡ λb.[b/a]L \mbox{ ;; } b \notin FV(L) \\ [y/x]M ≡ [y/x]λa.L ≡ λa.[y/x]L ~ \cdots (A) \\ \mbox{(条件より} y \notin FV(L) \mbox{ なので 1.12(g) はおこらない)} \\ [y/x]M^\prime ≡ [y/x]λb.[b/a]L ≡ λb.[y/x][b/a]L \\ \mbox{;; Lemma1.16(d) } [P/x][Q/y]M ≡ [Q/y][P/x]M ~ y \notin FV(P), ~ x \notin FV(Q) \mbox{ より} \\ \mbox{;; } a \notin FV(y), ~ x \notin FV(b) \mbox{ なので}\\ ≡ λb.[b/a][y/x]L ~ \cdots (B) \\ \mbox{(条件より} y \notin FV(L) \mbox{ なので 1.12(g) はおこらない)} \\ \mbox{帰納法により } [y^\prime/x^\prime]L^\prime \rhd_{\alpha0} [b^\prime/a^\prime][y^\prime/x^\prime]L^\prime \\ \mbox{が正しいと仮定して以下を導きます} \\ \mbox{(A), (B) は定義から } λa.[y/x]L \rhd_{\alpha0} λb.[b/a][y/x]L \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$(7)M ≡ (PQ)$ の時

$\begin{array} & M^\prime ≡ (RS) \mbox{ とする} \\ [y/x]M ≡ [y/x](PQ) ≡ ([y/x]P [y/x]Q) \\ [y/x]M^\prime ≡ [y/x](RS) ≡ ([y/x]R [y/x]S) \\ \mbox{帰納法により } \\ [y^\prime/x^\prime]P^\prime \rhd_{\alpha0} [y^\prime/x^\prime]R^\prime, ~ [y^\prime/x^\prime]Q^\prime \rhd_{\alpha0} [y^\prime/x^\prime]S^\prime \mbox{ が正しいと仮定して以下を導きます} \\ (PQ) \rhd_{\alpha0} (RS) \end{array}$

$\mbox{(1)〜(7) より 条件の時、} M \rhd_{\alpha0} M^\prime, ~ [y/x]M \rhd_{\alpha0} [y/x]M^\prime.$

“Lambda-Calculus and Combinators: An Introduction”メモ(その4)

Excercise A1.3

$S$ は β-redex であり、あらかじめ β-reduction をしておくもの。

$\begin{array} & P^\prime & ≡ & (λx.S)v, \mbox{ where } S ≡ (λyv.uvy)x \\ S & ≡ & (λy.(λv.uvy))x \\ & \rhd_{1\beta} & [x/y]λv.uvy \\ & ≡ & λv.uvx \\ P & ≡ & (λx.(λv.uvx))v \\ & \rhd_{1\beta} & [v/x](λv.uvx) \\ & ≡ & λy.[v/x][y/v]uvx \\ & ≡ & λy.[v/x]uyx \\ & ≡ & λy.uyv \\ \end{array}$

$S$ をそのまま $P^\prime$ へ代入するもの。

$\begin{array} & P^\prime & ≡ & (λx.(λyv.uvy)x)v \\ & \rhd_{1\beta} & [v/x](λyv.uvy)x \\ & ≡ & (λyv.uvy)v \\ & ≡ & (λy.(λv.uvy))v \\ & \rhd_{1\beta} & [v/y](λv.uvy) \\ & ≡ & λx.[v/y][x/v]uvy \\ & ≡ & λx.[v/y]uxy \\ & ≡ & λx.uxv \\ \end{array}$

“Lambda-Calculus and Combinators: An Introduction”メモ(その3)

Lemma 1.16

$1.12(g)$ is never used in the substitunion.

Lemma 1.16(a)
$\mbox{(a) } [P/v][v/x]M ≡ [P/x]M \mbox{ if } v \notin FV(M);$

$1.12$ をあてはめます。

$\begin{array} & \mbox{(1) } M=x \mbox{ の時 (1.12(a))} \\ \mbox{左辺 } [P/v][v/x]x = [P/v]v = P \\ \mbox{右辺 } [P/x]x = P \\ \therefore \mbox{(1)の時、左辺 ≡ 右辺} \\ \mbox{(2) } M=a \mbox{ の時 (1.12(b)) } \\ \mbox{左辺 } [P/v][v/x]a = [P/v]a = a \\ \mbox{右辺 } [P/x]a = a \\ \therefore \mbox{(2)の時、左辺 ≡ 右辺} \\ \mbox{(3) } M=(RS) \mbox{ の時 (1.12(c))} \\ \mbox{左辺 } [P/v][v/x](RS) = [P/v]([v/x]R [v/x]S) \\ = ([P/v][v/x]R [P/v][v/x]S) \\ \mbox{;; ここで帰納法により } \\ \mbox{;; } [Z/w][w/u]N ≡ [Z/u]N \\ \mbox{;; が正しいと仮定して以下を導きます} \\ = ([P/x]R \, [P/x]S) \\ \mbox{右辺 } [P/x](RS) = ([P/x]R \, [P/x]S) \\ \therefore \mbox{(3)の時、左辺 ≡ 右辺} \\ \mbox{(4) } M=λx.L \mbox{ の時 (1.12(d))} \\ \mbox{左辺 } [P/v][v/x](λx.L) = [P/v](λx.L) \\ \mbox{;; ここで条件 } v \notin FV(M) \mbox{ より} \\ \mbox{;; } v \notin FV(λx.L) \Rightarrow v \notin FV(L) \mbox{ だから } \\ = λx.L \\ \mbox{右辺 } [P/x](λx.L) = λx.L \\ \therefore \mbox{(4)の時、左辺 ≡ 右辺} \\ \mbox{(5) } M=λy.L, \; x \notin FV(L) \mbox{ の時 (1.12(e))} \\ \mbox{左辺 } [P/v][v/x](λy.L) = [P/v](λy.L) \\ \mbox{;; ここで条件 } v \notin FV(M) \mbox{ より} \\ \mbox{;; } v \notin FV(λy.L) \Rightarrow v \notin FV(L) \mbox{ だから } \\ = λy.L \\ \mbox{右辺 } [P/x](λy.L) = λy.L \\ \therefore \mbox{(5)の時、左辺 ≡ 右辺} \\ \mbox{(6) } M=λy.L, \; x \in FV(L) \mbox{ and } y ≠ x \mbox{ (1.12(f)) では} \\ \mbox{;; “and let no variable bound in M be free in vPQ.” つまり} \\ \mbox{;; } y \notin FV(vPQ) \mbox{ より} \\ \mbox{;; 特に } y \notin FV(PQ) \mbox{ より} \\ \mbox{左辺 } [P/v][v/x](λy.L) = [P/v](λy.[v/x]L) = λy.[P/v][v/x]L \\ \mbox{;; ここで帰納法により } \\ \mbox{;; } [Z/w][w/u]N ≡ [Z/u]N \\ \mbox{;; が正しいと仮定して以下を導きます} \\ = λy.[P/x]L \\ \mbox{右辺 } [P/x](λy.L) \\ \mbox{;; (6)の左辺と同様に} \\ \mbox{;; “and let no variable bound in M be free in vPQ.” つまり} \\ \mbox{;; } y \notin FV(vPQ) \mbox{ より} \\ = λy.[P/x]L \\ \therefore \mbox{(6)の時、左辺 ≡ 右辺} \\ \mbox{(1) 〜 (6) より } [P/v][v/x]M ≡ [P/x]M \mbox{ if } v \notin FV(M). \end{array}$
Lemma 1.16(b)
$\mbox{(b) } [x/v][v/x]M ≡ M \mbox{ if } v \notin FV(M);$

Part $(b)$ follows from $(a)$ and $1.15(a)$

$\begin{array} & \mbox{(a) より} \\ \mbox{左辺 } [x/v][v/x]M = [x/x]M \\ \mbox{1.15(a) より } [x/x]M ≡ M \mbox{ だから} \\ = M \\ \therefore \mbox{左辺 ≡ 右辺 なので} \\ [x/v][v/x]M ≡ M \mbox{ if } v \notin FV(M);. \end{array}$
Lemma 1.16(c)
$\mbox{(c) } [P/x][Q/y]M ≡ [([P/x]Q)/y][P/x]M \mbox{ if } y \notin FV(P);$

$1.12$ をあてはめます。

$\begin{array} & \mbox{(1) } M=x \mbox{ の時 (1.12(a))} \\ \mbox{左辺 } [P/x][Q/y]x = [P/x]x = P \\ \mbox{右辺 } [([P/x]Q)/y][P/x]x = [([P/x]Q)/y]P \\ \mbox{;; ここで } y \notin FV(P) \mbox{ なので } \\ = P \\ \therefore \mbox{(1)の時、左辺 ≡ 右辺} \\ \mbox{(1)' } M=y \mbox{ の時 (1.12(a))} \\ \mbox{左辺 } [P/x][Q/y]y = [P/x]Q \\ \mbox{右辺 } [([P/x]Q)/y][P/x]y = [([P/x]Q)/y]y = [P/x]Q \\ \therefore \mbox{(1)'の時、左辺 ≡ 右辺} \\ \mbox{(2) } M=a \mbox{ の時 (1.12(b))} \\ \mbox{左辺 } [P/x][Q/y]a = [P/x]a = a \\ \mbox{右辺 } [([P/x]Q)/y][P/x]a = [([P/x]Q)/y]a = a \\ \therefore \mbox{(2)の時、左辺 ≡ 右辺} \\ \mbox{(3) } M=(RS) \mbox{ の時 (1.12(c))} \\ \mbox{左辺 } [P/x][Q/y](RS) = [P/x]([Q/y]R [Q/y]S) \\ = ([P/x][Q/y]R \, [P/x][Q/y]S) \\ \mbox{;; ここで帰納法により } \\ \mbox{;; } [V/w][Z/u]N ≡ [([V/w]Z)/u][V/w]N \mbox{ if } u \notin FV(V); \\ \mbox{;; が正しいと仮定して以下を導きます} \\ = ([([P/x]Q)/y][P/x]R \, [([P/x]Q)/y][P/x]S) \\ \mbox{右辺 } [([P/x]Q)/y][P/x](RS) = [([P/x]Q)/y]([P/x]R [P/x]S) \\ = ([([P/x]Q)/y][P/x]R \, [([P/x]Q)/y][P/x]S) \\ \therefore \mbox{(3)の時、左辺 ≡ 右辺} \\ \mbox{(4) } M=λx.L \mbox{ の時 (1.12(d), 1.12(f))} \\ \mbox{左辺 } [P/x][Q/y](λx.L) \\ \mbox{;; 1.12(f) より} \\ = [P/x](λx.[Q/y]L) \\ \mbox{;; 1.12(d) より} \\ = λx.[Q/y]L \\ \mbox{右辺 } [([P/x]Q)/y][P/x](λx.L) \\ \mbox{;; 1.12(d) より} \\ = [([P/x]Q)/y](λx.L) \\ \mbox{;; 1.12(f) より} \\ = λx.[([P/x]Q)/y]L \\ \mbox{;; ここで定義} \\ \mbox{;; “and let no variable bound in M be free in vPQ.” つまり} \\ \mbox{;; } x \notin FV(vPQ) \mbox{ 特に } x \notin FV(Q) \mbox{ より} \\ = λx.[Q/y]L \\ \therefore \mbox{(4)の時、左辺 ≡ 右辺} \\ \mbox{(4)' } M=λy.L \mbox{ の時 (1.12(d), 1.12(f))} \\ \mbox{左辺 } [P/x][Q/y](λy.L) \\ \mbox{;; 1.12(d) より} \\ = [P/x](λy.L) \\ \mbox{;; 1.12(f) より} \\ = λy.[P/x]L \\ \mbox{右辺 } [([P/x]Q)/y][P/x](λy.L) \\ \mbox{;; 1.12(f) より} \\ = [([P/x]Q)/y](λy.[P/x]L) \\ \mbox{;; 1.12(d) より} \\ = λy.[P/x]L \\ \therefore \mbox{(4)'の時、左辺 ≡ 右辺} \\ \mbox{(5) } M=λz.L, x \notin FV(L), y \notin FV(L) \mbox{ の時 (1.12(e)))} \\ \mbox{左辺 } [P/x][Q/y](λz.L) = λz.L \\ \mbox{右辺 } [([P/x]Q)/y][P/x](λz.L) = λz.L \\ \therefore \mbox{(4)''の時、左辺 ≡ 右辺} \\ \mbox{・1.12(g) について} \\ (g) [N/x](λy.P) ≡ λz.[N/x][z/y]P \mbox{ if } x \in FV(P), y \in FV(N) \\ \mbox{ここで定義 “and let no variable bound in M be free in vPQ.” つまり} \\ x \notin FV(vPQ) \mbox{ 特に } x \notin FV(PQ) \mbox{ より} \\ \mbox{1.12(g) は成り立たない.} \\ \therefore \mbox{(1)〜(5) より} \\ [P/x][Q/y]M ≡ [([P/x]Q)/y][P/x]M \mbox{ if } y \notin FV(P);. \end{array}$
Lemma 1.16(d)
$\mbox{(d) } [P/x][Q/y]M ≡ [Q/y][P/x]M \mbox{ if } y \notin FV(P), x \notin FV(Q);$

$(d)$ follows from $(c)$ and $1.15(b)$

$\begin{array} & \mbox{左辺 } [P/x][Q/y]M \\ \mbox{(c) } [P/x][Q/y]M ≡ [([P/x]Q)/y][P/x]M \mbox{ if } y \notin FV(P); \mbox{ より} \\ = [([P/x]Q)/y][P/x]M \\ \mbox{;; ここで 1.15(b): } \\ x \notin FV(M) \Rightarrow [N/x]M ≡ M \mbox{ より} \\ \mbox{;; 特に } x \notin FV(Q) \Rightarrow [P/x]Q ≡ Q \\ = [Q/y][P/x]M \mbox{;; これは右辺に等しい} \\ \therefore [P/x][Q/y]M ≡ [Q/y][P/x]M \mbox{ if } y \notin FV(P), x \notin FV(Q);. \end{array}$
Lemma 1.16(e)
$\mbox{(e) } [P/x][Q/x]M ≡ [([P/x]Q)/x]M$

$1.12$ をあてはめます。

$\begin{array} & \mbox{(1) } M=x \mbox{ の時 (1.12(a))} \\ \mbox{左辺 } [P/x][Q/x]x = [P/x]Q \\ \mbox{右辺 } [([P/x]Q)/x]x = [P/x]Q \\ \therefore \mbox{(1)の時、左辺 ≡ 右辺} \\ \mbox{(2) } M=a \mbox{ の時 (1.12(b))} \\ \mbox{左辺 } [P/x][Q/x]a = [P/x]a = a \\ \mbox{右辺 } [([P/x]Q)/x]a = a \\ \therefore \mbox{(2)の時、左辺 ≡ 右辺} \\ \mbox{(3) } M=(RS) \mbox{ の時 (1.12(c))} \\ \mbox{左辺 } [P/x][Q/x](RS) = [P/x]([Q/x]R [Q/x]S) \\ = ([P/x][Q/x]R \, [P/x][Q/x]S) \\ \mbox{;; ここで帰納法により } \\ \mbox{;; } [V/w][Z/w]N ≡ [([V/w]Z)/w]N \\ \mbox{;; が正しいと仮定して以下を導きます} \\ = ([([P/x]Q)/x]R \, [([P/x]Q)/x]S) \\ \mbox{右辺 } [([P/x]Q)/x](RS) \\ = ([([P/x]Q)/x]R \, [([P/x]Q)/x]S) \\ \therefore \mbox{(3)の時、左辺 ≡ 右辺} \\ \mbox{(4) } M=λx.L \mbox{ の時 (1.12(d))} \\ \mbox{左辺 } [P/x][Q/x](λx.L) = [P/x](λx.L) = λx.L \\ \mbox{右辺 } [([P/x]Q)/x](λx.L) = λx.L \\ \therefore \mbox{(4)の時、左辺 ≡ 右辺} \\ \mbox{(5) } M=λy.L, \; x \notin FV(L) \mbox{ の時 (1.12(e))} \\ \mbox{左辺 } [P/x][Q/x](λy.L) = [P/x](λy.L) = λy.L \\ \mbox{右辺 } [([P/x]Q)/x](λy.L) = λy.L \\ \therefore \mbox{(5)の時、左辺 ≡ 右辺} \\ \mbox{(6) } M=λy.L, \; x \in FV(L) \mbox{ and } y ≠ x \mbox{ (1.12(f))} \\ \mbox{;; “and let no variable bound in M be free in vPQ.” つまり} \\ \mbox{;; } y \notin FV(PQ) \mbox{ より} \\ \mbox{左辺 } [P/x][Q/x](λy.L) = [P/x](λy.[Q/x]L) = λy.[P/x][Q/x]L \\ \mbox{;; ここで帰納法により } \\ \mbox{;; } [V/w][Z/w]N ≡ [([V/w]Z)/w]N \\ \mbox{;; が正しいと仮定して以下を導きます} \\ = λy.[([P/x]Q)/x]L \\ \mbox{右辺 } [([P/x]Q)/x](λy.L) \\ \mbox{;; (6)の左辺と同様に} \\ \mbox{;; “and let no variable bound in M be free in vPQ.” つまり} \\ \mbox{;; } y \notin FV(vPQ) \mbox{ より} \\ \mbox{;; 特に } y \notin FV(PQ) \mbox{ より} \\ = λy.[([P/x]Q)/x]L \\ \therefore \mbox{(6)の時、左辺 ≡ 右辺} \\ \mbox{(1) 〜 (6) より } [P/x][Q/x]M ≡ [([P/x]Q)/x]M. \end{array}$

“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)$ が成り立つ、成り立たない場合を両方考えます。

“Lambda-Calculus and Combinators: An Introduction”メモ

J. Roger Hindley, Homepage — http://www.users.waitrose.com/~hindley/ 著者の一人が ICL2 と略しておられるのでそれを使わせて頂きます。ICL2 1章の気付きポイントのメモと練習問題の写経など。

By the way, the expression ‘$λ$’ by itself is not a term, though it may occur in terms; similarly the expression ‘$λx$’ is not a term.

Exercise 1.4

省略表記された λ-term の括孤とλを補う問題。

$\begin{array} & \mbox{(a) } xyz(yx) \\ ≡ \Big(((xy)z)(yx)\Big) \\ \\ \mbox{(b) } λx.uxy \\ ≡ \Big(λx.((ux)y)\Big) \\ \\ \mbox{(c) } λu.u(λx.y) \\ ≡ \Big(λu.(u(λx.y))\Big) \\ \\ \mbox{(d) } (λu.vuu)zy \\ ≡ \Big(\Big((λu.((vu)u))z\Big)y\Big) \\ \\ \mbox{(e) } ux(yz)(λv.vy) \\ ≡ \Big(((ux)(yz))(λv.(vy))\Big) \\ \\ \mbox{(f) } (λxyz.xz(yz))uvw \\ ≡ \Big(\Big(\Big(\Big(λx.(λy.(λz.((xz)(yz))))\Big)u\Big)v\Big)w\Big) \\ \\ \end{array}$

Exercise 1.8

省略表記された λ-term の括孤とλを補うことがヒント。

$\begin{array} & \mbox{(a) 以下の λ-termの xy に下線を付ける} \\ λxy.xy \\ ≡ (λx.(λy.(\underline{xy}))) \\ \\ \mbox{(b) uv に下線を付ける} \\ x(uv)(λu.v(uv))uv \\ ≡ ((((x(\underline{uv}))(λu.(v(\underline{uv}))))u)v) \\ \\ \mbox{(c) 以下の λ-term に λu.u が存在するかどうか} \\ λu.u \\ ≡ (λu.u), \\ λu.uv \\ ≡ (λu.(uv)) \mbox{これには λu.u は存在しない} \end{array}$

Exercise 1.14

$(c)$ は Definition 1.12 (Substitution) から Remark 13 で特に解説されたもの。

$\begin{array} & \mbox{(a) } [(uv)/x](λy.x(λw.vwx)) \\ ≡ λy.(uv)(λw.vw(uv)) \\ \\ \mbox{(b) } [(λy.xy)/x](λy.x(λx.x)) \\ ≡ λy.(λy.xy)(λx.x) \\ \\ \mbox{(c) } [(λy.vy)/x](y(λv.xv)) \\ ≡ y[(λy.vy)/x](λv.xv) \\ ≡ y(λz.[(λy.vy)/x][z/v]xv) \\ ≡ y(λz.(λy.vy)z) \\ ;; \mbox{解答では、 z ≠ x,y,v。ただ、Definition 1.12 から} \\ ;; z \notin FV((λy.vy)(xv)) \mbox{ を満たすもので良いので } z \notin \{x, v\}\\ \\ \mbox{(c)別解 } [(λy.vy)/x](y(λv.xv)) \\ ≡ y[(λy.vy)/x](λv.xv) \\ ≡ y(λy.[(λy.vy)/x][y/v]xv) \\ ≡ y(λy.(λy.vy)y) \\ ;; \mbox{z の替わりに y と置いた場合でも満たしているのがわかる} \\ \\ \mbox{(d) } [(uv)/x](λx.zy) \\ ≡ λx.zy \\ \end{array}$