SK言語

Theorem1.
全てのTree(xn)に対して
Tree(xn) = G(S,K)Tree' xn...xn
となる,Tree'が存在する

proof.
書き換え(0) X = (K X xn) … ※Tree(xn)がxnを含まない場合
書き換え(1) (xn Y) = (R Y xn)
書き換え(2) F (G xn) = B F G xn
を使う


Theorem2.
全てのTree(xn)に対して
Tree(xn) = G(S,K)Tree' xn
となるG,Tree'が存在する

proof.
Theorem1.を使うと F xn...xn の形になっている。
F xn xn = SFI xn を繰り返し使えばよい。

Theorem3.
Tree(x1,...,xn)= Tree' x1,...,xnとなるTree'が存在する
xn,x[n-1],...x1の変数にに対してTheorem2を使う。

Theorem4.
F x1 x2 x3...xn = Tree(x1,...,xn,F) に対して
F x1 x2 x3...xn = Tree' x1 x2...xn となる Tree'が存在する

Therem5.から
F x1 x2 x3...xn = Tree'' F x1 x2...xn となる Tree''が存在する
F = Tree'' F なので不動点コンビネータYを使い
F = Y Tree'' とすればよい。