SおよびKコンビネータだけで任意のλ式が書ける

証明は単純だった．

It is a perhaps astonishing fact that S and K can be composed to produce combinators that are extensionally equal to any lambda term, and therefore, by Church's thesis, to any computable function whatsoever. The proof is to present a transformation, T[ ], which converts an arbitrary lambda term into an equivalent combinator.

こうなると一見さんも遊べるようにJavaScriptで自動変換を書きたくなる．どっかにないのかな？ でもひどく長くなるらしい．

In general, the T[ ] construction may expand a lambda term of length n to a combinatorial term of length Θ(3ⁿ).