コンビネータ論理
もっとも単純なコンビネータの例は、以下のように定義される恒等コンビネータIである。
(I x) = x
もうひとつの単純なコンビネータはKで、定数関数を作る。(K x)はどんな引数に対してもxを返す関数である。そして、Kはこのように定義する:
((K x) y) = x
もしくは、伝統的な複数の適用の表記に従えば
(K x y) = x
三つ目のコンビネータは、適用を一般化したSである。
(S x y z) = (x z (y z))
Sは、それぞれにzを適用したあとxをyに適用する。別の言い方をすれば、zという環境においてxをyに適用する。 SとKがあれば、Iは不必要である。なぜなら、他の二つでこのようにして表現できるからである。
((S K K) x) = (S K K x) = (K x (K x)) = x
すべての項xに対して((S K K) x) = (I x)が成り立つが、(S K K)自身はIとは同じではない。これらの項は外延的に同値である。外延的同値は関数の同値という数学的な概念である。二つの関数が、同じ引数に対して常に同じ結果を返すならばそれは等しい。対照的に、原始的なコンビネータと一緒にあるそれらの項自身は、内包的同値という概念を捉える。十分な引数が与えられたときに、原始的なコンビネータに展開されるまで同じ形をもつ時だけ、それらは同値である。
恒等関数を実装するにはたくさんの方法がある。(S K K)とIはそれに含まれている。さらに、(S K S)もそうである。今後、同値という言葉を外延的同値を示し、等しいを同じコンビネータを示すのに使う。
さらに面白いコンビネータは、再帰を実装するために使える不動点コンビネータ(Yコンビネータ)である。
Tは抽象を消去することが動機となっている。規則3、4は自明である:λx.xは明らかにIと等しく、λx.Eはxが自由変数としてEに出現しない時明らかに(KT[E])である。 最初の二つの規則も単純である。変数はそれ自身に変換され、コンビネータ項において許されている適用は単にアプリカンドとコンビネータへの引数の変換である。 5番目と6番目の規則は興味深い。5番目は複雑な抽象をコンビネータに変換することを単純に示している。まず本体をコンビネータに変換し、それから抽象を除去する。6番目は実際に抽象を除去する。 λx.(E1 E2)はaという引数を取り、ラムダ項(E1 E2)のxを置き換えて (E1 E2)[x : = a]を生成する関数である。 しかし、(E1 E2)の中のxをaで置き換えるのはちょうどE1 and E2を置き換えるのと同じである。だから
外延的同値性によって、
したがって、λx.(E1 E2)と等しいコンビネータを見つけるには、(S λx.E1 λx.E2)と等しいコンビネータを探せば十分である。そして
は明らかにその要件に適合する。E1とE2がそれぞれ(E1 E2)より厳密に少ない適用を含むため、再帰はすべての変数及びλx.Eの形の項において終了させなければならない。