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