$M_{1} ≡ y(λx.xy(λzw.yz))$

$w,x,y,z$ が出現しているので、$w \to v, x \to v', y \to v'', z \to v'''$とするとして、
$M_{1} ≡ (v''(λv'(v'(v''(λv'''(λv(v''v'''))))))).$

$M_{2} ≡ λv'(λv''((((λvv)v')v'')((v''(λv'''(v'v''')))v'')))$

同様に、 $w \gets v, x \gets v', y \gets v'', z \gets v'''$ とするとして、
$M_{2} ≡ λxy.((λw.w)xy(y(λz.xz)y)).$

まず何が問題なのか、つまり、どのように証明するのかよくわからない。そこで以下を参考にします。

考え方は、 substitution の定義から、構造的帰納法で証明する、ということらしい。解答そのものも記述があるので、それを写経します。

基底ケースの variable について左辺と右辺が等しいことを導いた後、 application と abstraction について帰納法で証明しています。これが、この問題の証明となります。再帰関数の定義と同様な方法を用いていて証明する、ということを考えれば納得できます。この場合、どこが基底で、どこが帰納（関数でいう再帰呼び出しするところという程度の認識です）を見出すことができなかったということをもって、何が問題なのかが理解できなかったということです。

以下写経します。

まず、 $M=x$ を考えます。

次に、 $M=y.$

次に考えるのが、 $M=z, z ≠ x \land z ≠ y.$これを示す必要があります。

ここまで、基底ケースの variable について左辺と右辺が等しいことは導かれました。あとは、 application と abstraction を帰納法で導いていくことになります。

$M = (M_{1}M_{2})$、 application について。

ここで帰納法により、 $X[x:=N][y:=L] \; = \; X[y:=L][x:=N[y:=L]]$ が正しいと仮定して、以下を導きます。

これは右辺と等しい。

$M = λz.M'$ つまり abstraction について。ここで、$z$ の条件として $z ≠ x \land z ≠ y$を挙げています。

ここで帰納法により、 $X[x:=N][y:=L] \; = \; X[y:=L][x:=N[y:=L]]$ が正しいと仮定して、以下を導きます。

これは右辺と等しい。

以上により $M[x:=N][y:=L] \; ≡ \; M[y:=L][x:=N[y:=L]]$ が証明されました。もう一度書くと、 substitution の定義から、 variable, application, と abstraction についてそれぞれ証明されたわけです。

(i) 2.2を用いて、と書いてある、ということは取り合えず脇に置いておいて、問うていることを自分なりに冗長に記述していきます。

これが意味しているのは、例で示されているものを見ると、 ある式$M$について、式$M$中に現れる$M_{1}$を$M_{2}$で置き換えても、置き換えられたそれぞれの式は=の関係になる、ということのようなので、$(λx.M)M_{1} = (λx.M)M_{2}$ つまり、

が成り立つ、ということのようなのだけれども、ここで言っている $λ\vdash$ や $=$ が意味している所が今の所の説明では厳密ではないと思うので、後続の章の後に考えることにします。！

こちらは 前回の記事で。

これ S を使えそうな気がします。 S を使って表すことを simplify と呼ぶのだろうか？という疑問はありまけれども…

$S$ で、この $x$ に渡る所の $z$ をどうにかできれば、 $B$ は $S$ で表すことができます、ということらしい。

参考 B,C,K,Wシステム — https://ja.wikipedia.org/wiki/B,C,K,W%E3%82%B7%E3%82%B9%E3%83%86%E3%83%A0 等。

$K$ を上手に使って、いわゆる二つ目の引数となる項を無視しています。成程、よく思い付くなこれ。

※ここで $λ\vdash$ と $=$ は、 application や abstraction を書き換えていくと、結局、 $M = X(YZ) = N$ という、字面が同じ λ-term になる、という程の意味で使っています。

ここでも simplify というのだけれども、この意味がいまいちわからない…

$\mbox{(i) } λ\vdash KI = K_{*}$

左辺を考えると、

$\mbox{(ii) } λ\vdash SKK = I$

左辺を考えると、