“Introduction to Lambda Calculus” メモ(その2)
2章の練習問題の前にある証明の問題の二つです。自分なりに解いてみたものです。
$A_{+} ≡ λmnfx.mf(nfx)$ のとき $A_{+}C_{m}C_{n} = C_{m+n}$ の証明
$\mbox{(1) } m=1$ のとき
$\begin{array} &
A_{+}C_{1}C_{n} \\
= λfx.C_{1}f(C_{n}fx) \mbox{ ; } [C_{1}:=λfx.fx] \downarrow \\
= λfx.((λfx.fx)f)(C_{n}fx) \\
= λfx.(λx.fx)(C_{n}fx) \\
= λfx.f (C_{n}fx) \mbox{ ; 2.1.4 の (ii)より} \downarrow \\
= λfx.f(f^{n}x) \\
\mbox{ 2.1.4 の (i) より} \\
≡ C_{n+1}.
\end{array}$
$\mbox{(2) } m=k$ のとき命題が成り立つと仮定すると $A_{+}C_{k}C_{n} = C_{k+n}.$
ここで $m=k+1$ を考えます。 $A_{+}C_{k+1}C_{n} = A_{+}(A_{+}C_{1}C_{k})C_{n}$から
$\begin{array} &
A_{+}C_{k+1}C_{n} \\
= A_{+}(A_{+}C_{1}C_{k})C_{n} \\
A_{+}C_{1}C_{k} = λfx.f(f^{k}x) = λfx.f(C_{k}fx) \mbox{ なので} \\
= A_{+}(λfx.f(C_{k}fx))C_{n} \\
= λfx.( (λfx.f(C_{k}fx))f)(C_{n}fx) \\
= λfx.(λx.f(C_{k}fx))(C_{n}fx) \\
= λfx.f(C_{k}f(C_{n}fx)) \\
= λfx.f((λfx.C_{k}f(C_{n}fx))fx) \\
= λfx.f(A_{+}C_{k}C_{n}fx) \\
\mbox{ここで仮定} A_{+}C_{k}C_{n} = C_{k+n} \mbox{より} \\
= λfx.f(C_{k+n}fx) \\
= λfx.f(f^{k+n}x) \\
≡ C_{k+n+1}. \\
\\
\\
\mbox{(1),(2)より} \\
A_{+}C_{1}C_{n} = C_{1+n}, \\
A_{+}C_{k+1}C_{n} = C_{k+1+n}. \\
\therefore \forall m \; A_{+}C_{m}C_{n} = C_{m+n}.
\end{array}$
$A_{*} ≡ λxyz.x(yz)$ のとき $A_{*}C_{m}C_{n} = C_{m*n}$ の証明
$(a)$ 右辺は $C_{m*n} = λfx.f^{m*n}(x)$.
左辺を考えると、
$\begin{array} &
A_{*}C_{m}C_{n} \\
= λf.C_{m}(C_{n}f) \\
= λf.(λfx.f^{m}(x))(C_{n}f) \\
= λf.(λx.(C_{n}f)^{m}(x)) \\
\mbox{ここで補助定理} (C_{n}x)^{m}(y) = x^{n*m}(y) \mbox{より} \\
= λf.(λx.f^{n*m}(x)) \\
= λfx.f^{n*m}(x). \\
(a) \mbox{より、これは右辺と同じ} \\
\therefore A_{*}C_{m}C_{n} = C_{m*n}. \\
\end{array}$