“Introduction to Lambda Calculus” メモ(その4)
感想としては外に当たらないと解答できないような問題は解けるわけがないよ、というところでした…
問題2.9
$MNL$ は（特に次の問題との対比で）どうやら、 free な variable を含む λ-term であるかもしれない、ということになると考えられます。つまり、$F$ を λ-term で素直に abstraction にすることができない。
例えば、 $F = λmn.m(nm)n$ とすると、 $n$ に $m$ が free な variable を含む λ-term だった場合。 closed λ-term と陽に closed であることを問題にしているのだろうと考えました。
これの Completeness of the S-K basis の所。任意の λ-term は、$S$ と $K$ の組み合わせで表現することができる、ということで、以下が示されています。
$\begin{array} &
\mbox{(1) } T[x] \Rightarrow x \\
\mbox{(2) } T[(E_{1}E_{2})] \Rightarrow (T[E_{1}] T[E_{2}]) \\
\mbox{(3) } T[λx.E] \Rightarrow (K T[E]) \mbox{ (if x does not occur free in E)} \\
\mbox{(4) } T[λx.x] \Rightarrow I \\
\mbox{(5) } T[λx.λy.E] \Rightarrow T[λx.T[λy.E]] \mbox{ (if x occurs free in E)} \\
\mbox{(6) } T[λx.(E_{1}E_{2})] \Rightarrow (S T[λx.E_{1}] T[λx.E_{2}])
\end{array}$
以下が示される例。
$\begin{array} &
T[λx.λy.(yx)] \\
= T[λx.T[λy.(y x)]] \mbox{ (by 5)} \\
= T[λx.(S T[λy.y] T[λy.x])] \mbox{ (by 6)} \\
= T[λx.(S I T[λy.x])] \mbox{ (by 4)} \\
= T[λx.(S I (K x))] \mbox{ (by 3 and 1)} \\
= (S T[λx.(S I)] T[λx.(K x)]) \mbox{ (by 6)} \\
= (S (K (S I)) T[λx.(K x)]) \mbox{ (by 3)} \\
= (S (K (S I)) (S T[λx.K] T[λx.x])) \mbox{ (by 6)} \\
= (S (K (S I)) (S (K K) T[λx.x])) \mbox{ (by 3)} \\
= (S (K (S I)) (S (K K) I)) \mbox{ (by 4)}
\end{array}$
$S,K,I$ で示すことができたので、これに今度は $x, y$ を適用しています。
$\begin{array} &
(S (K (S I)) (S (K K) I) x y) \\
= (K (S I) x (S (K K) I x) y) \\
= (S I (S (K K) I x) y) \\
= (I y (S (K K) I x y)) \\
= (y (S (K K) I x y)) \\
= (y (K K x (I x) y)) \\
= (y (K (I x) y)) \\
= (y (I x)) \\
= (y x) \\
\end{array}$
というわけで、問題 $\mbox{(i) }F ≡ λmn.m(nm)n$ 。
$\begin{array} &
T[λmn.m(nm)n] \\
= T[λm.λn.m(nm)n] \\
= T[λm.T[λn.m(nm)n]] \\
= T[λm.(S T[λn.(m(nm))] T[λn.n])] \\
= T[λm.(S (S T[λn.m] T[λn.(nm)]) T[λn.n])] \\
= T[λm.(S (S (K m) T[λn.(nm)]) T[λn.n]) \\
= T[λm.(S (S (K m) (S T[λn.n] T[λn.m])) T[λn.n]) \\
= T[λm.(S (S (K m) (S I T[λn.m])) T[λn.n]) \\
= T[λm.(S (S (K m) (S I (K m))) T[λn.n]) \\
= T[λm.(S (S (K m) (S I (K m))) I) \\
= (S T[λm.(S (S (K m) (S I (K m))))] T[λm.I]) \\
= (S (S T[λm.S] T[λm.(S (K m) (S I (K m)))]) T[λm.I]) \\
= (S (S (K S) T[λm.(S (K m) (S I (K m)))]) T[λm.I]) \\
= (S (S (K S) T[λm.((S (K m)) (S I (K m)))]) T[λm.I]) \\
= (S (S (K S) (S T[λm.(S (K m))] T[λm.(S I (K m))])) T[λm.I]) \\
= (S (S (K S) (S (S T[λm.S] T[λm.(K m)]) T[λm.(S I (K m))])) T[λm.I]) \\
= (S (S (K S) (S (S (K S) T[λm.(K m)]) T[λm.(S I (K m))])) T[λm.I]) \\
= (S (S (K S) (S (S (K S) (S T[λm.K] T[λm.m])) T[λm.(S I (K m))])) T[λm.I]) \\
= (S (S (K S) (S (S (K S) (S (K K) T[λm.m])) T[λm.(S I (K m))])) T[λm.I]) \\
= (S (S (K S) (S (S (K S) (S (K K) I)) T[λm.(S I (K m))])) T[λm.I]) \\
= (S (S (K S) (S (S (K S) (S (K K) I)) T[λm.((S I) (K m))])) T[λm.I]) \\
= (S (S (K S) (S (S (K S) (S (K K) I)) (S T[λm.(S I)] T[λm.(K m)]))) T[λm.I]) \\
= (S (S (K S) (S (S (K S) (S (K K) I)) (S (K (S I)) T[λm.(K m)]))) T[λm.I]) \\
= (S (S (K S) (S (S (K S) (S (K K) I)) (S (K (S I)) (S T[λm.K] T[λm.m])))) T[λm.I]) \\
= (S (S (K S) (S (S (K S) (S (K K) I)) (S (K (S I)) (S (K K) T[λm.m])))) T[λm.I]) \\
= (S (S (K S) (S (S (K S) (S (K K) I)) (S (K (S I)) (S (K K) I)))) T[λm.I]) \\
= (S (S (K S) (S (S (K S) (S (K K) I)) (S (K (S I)) (S (K K) I)))) (K I)) \\
\end{array}$
今度はこの結果に $m,n$ を適用します。
$\begin{array} &
Fmn \\
=((S (S (K S) (S (S (K S) (S (K K) I)) (S (K (S I)) (S (K K) I)))) (K I))m n) \\
=(S (K S) (S (S (K S) (S (K K) I)) (S (K (S I)) (S (K K) I))) m (K I m) n) \\
=(K S m (S (S (K S) (S (K K) I)) (S (K (S I)) (S (K K) I)) m) (K I m) n) \\
=(S (S (S (K S) (S (K K) I)) (S (K (S I)) (S (K K) I)) m) (K I m) n) \\
=(S (S (K S) (S (K K) I)) (S (K (S I)) (S (K K) I)) m n (K I m n)) \\
=(S (K S) (S (K K) I) m (S (K (S I)) (S (K K) I) m) n (K I m n)) \\
=(K S m (S (K K) I m) (S (K (S I)) (S (K K) I) m) n (K I m n)) \\
=(S (S (K K) I m) (S (K (S I)) (S (K K) I) m) n (K I m n)) \\
=(S (K K) I m n (S (K (S I)) (S (K K) I) m n) (K I m n)) \\
=(K K m (I m) n (S (K (S I)) (S (K K) I) m n) (K I m n)) \\
=(K (I m) n (S (K (S I)) (S (K K) I) m n) (K I m n)) \\
=((I m) (S (K (S I)) (S (K K) I) m n) (K I m n)) \\
=(m (S (K (S I)) (S (K K) I) m n) (K I m n)) \\
=(m (K (S I) m (S (K K) I m) n) (K I m n)) \\
=(m (S I (S (K K) I m) n) (K I m n)) \\
=(m (I n (S (K K) I m n)) (K I m n)) \\
=(m (n (S (K K) I m n)) (K I m n)) \\
=(m (n (K K m (I m) n)) (K I m n)) \\
=(m (n (K (I m) n)) (K I m n)) \\
=(m (n (I m)) (K I m n)) \\
=(m (n m) (K I m n)) \\
=(m (n m) (I n)) \\
=(m (n m) n) \\
\end{array}$