“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 の条件と重なることになります。
“Lambda-Calculus and Combinators: An Introduction”メモ(その5)
Lemma A1.7
$M$ の構造的帰納法で証明します。
$(1) M ≡ x$ の時
$(2) M ≡ y$ の時
$(3) M ≡ a$ の時
$(4) M ≡ λx.L$ の時
$(5) M ≡ λy.L$ の時
$(6) M ≡ λa.L$ の時
$(7)M ≡ (PQ)$ の時
“Lambda-Calculus and Combinators: An Introduction”メモ(その4)
Excercise A1.3
$S$ は β-redex であり、あらかじめ β-reduction をしておくもの。
$S$ をそのまま $P^\prime$ へ代入するもの。
“Lambda-Calculus and Combinators: An Introduction”メモ(その3)
Lemma 1.16
$1.12(g)$ is never used in the substitunion.
Lemma 1.16(a)
$1.12$ をあてはめます。
Lemma 1.16(b)
Part $(b)$ follows from $(a)$ and $1.15(a)$
Lemma 1.16(c)
$1.12$ をあてはめます。
Lemma 1.16(d)
$(d)$ follows from $(c)$ and $1.15(b)$
Lemma 1.16(e)
$1.12$ をあてはめます。
“Lambda-Calculus and Combinators: An Introduction”メモ(その2)
Lemma 1.15
Proof Easy, by checking the clauses of Definition 1.12.
とあるので、実際やってみます。
Lemma 1.15(a)
Lemma 1.15(b)
$1.12(a)$ 成り立たない、という最初が肝心だと思う。
Lemma 1.15(c)
definition 1.12 を照らし合わせます。
つまり、 Lemma 1.15(c) に当てはまめて substitution しても $M$ に変化が無いものは除外して考えています。
Lemma 1.15(d)
$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 の括孤とλを補う問題。
Exercise 1.8
省略表記された λ-term の括孤とλを補うことがヒント。
Exercise 1.14
$(c)$ は Definition 1.12 (Substitution) から Remark 13 で特に解説されたもの。