コンビネータ論理

コンビネータ論理(Combinatory Logic、組み合わせ論理)は、モイセイ・シェインフィンケリ（露: Моисей Эльевич Шейнфинкель、英: Moses Ilyich Schönfinkel）とハスケル・カリー（英: Haskell Brooks Curry）によって、記号論理での変数を消去するために導入された記法である。最近では、計算機科学において計算の理論的モデルで利用されてきている。また、関数型プログラミング言語の理論（意味論など）や実装にも応用がある。
コンビネータ論理は、コンビネータまたは引数のみからなる関数適用によって結果が定義されている高階関数、コンビネータに基づいている。

数学におけるコンビネータ論理

コンビネータ論理は元来、本質的に量化変数を消去することによって量化変数の役割を明確にするような「pre-logic」を意図していた。量化変数を消去する方法にはクワインの述語関手論理がある。コンビネータ論理の表現力は一階述語論理を超える一方、述語関手論理の表現力は一階述語論理と同等である。
コンビネータ論理の最初の発明者であるモイセイ・シェインフィンケリは、1924年の論文以降それについて何も出版していない（ヨシフ・スターリンが1929年に権力を確固なものとしてからはほとんど出版を行なっていない）。1927年後半、カリーはプリンストン大学の講師として働いているときにコンビネータを再発見した。1930年代後半、アロンゾ・チャーチとプリンストン大学の彼の教え子が、ラムダ計算というライバルとなる関数抽象の形式化を考案し、コンビネータ論理より人気を博すこととなった。こうした歴史的偶然のために、理論計算機科学が60〜70年代にコンビネータ論理に関心を持ち始めるまで、この分野のほとんどすべての業績は、ほとんどカリーとその教え子、もしくはベルギーのロベール・フェイによるものであった。Curry and Feys (1958) および Curry et al. (1972)  はコンビネータ論理の初期の歴史についてのサーベイ論文である。より最近のコンビネータ論理とラムダ計算の比較については Barendregt (1984) を参照されたい（デイナ・スコットが60〜70年代に考案したコンビネータ論理のためのモデル理論についても触れている）。

計算機科学におけるコンビネータ論理

計算機科学において（計算可能性理論や証明論で）は、コンビネータ論理は計算を単純化したモデルとして使われる。単純にもかかわらず、コンビネータ論理は計算の本質的な特徴をとらえている。
コンビネータ論理はラムダ計算の変種としても見ることができる。ラムダ式(ラムダ抽象)は、束縛変数のない原始的な関数「コンビネータ」の有限集合によって置き換えられる。ラムダ式をコンビネータ式に変換するのは簡単であり、またコンビネータの簡約はラムダの簡約よりもシンプルである。したがってコンビネータ論理は非正格関数型言語やGraph reduction machineのモデルとして使われている。もっとも純粋な形は、唯一のプリミティブが入出力のために拡張されたSとKのコンビネータの、Unlambdaというプログラミング言語である。実用的なプログラミング言語ではないが、Unlambdaは理論的な関心がある。
コンビネータ論理は解釈の多様性を与えられる。カリーによる論文では、どのように従来の論理のための公理をコンビネータ論理の等式にするかを示した。デイナ・スコットは、60,70年代にどのようにしてモデル理論とコンビネータ論理を結びつけるかを示した。

コンビネータ計算

ラムダ抽象が関数を作るための唯一の方法だから、コンビネータ計算では何かでそれを置き換える必要がある。コンビネータ計算は、ラムダ抽象の代わりに、原始的な関数の有限集合を提供し、それらから他の関数を構成することができるようにしている。

T[ ] 変換について

Tは抽象を消去することが動機となっている。規則3、4は自明である:λx.xは明らかにIと等しく、λx.Eはxが自由変数としてEに出現しない時明らかに(KT[E])である。
最初の二つの規則も単純である。変数はそれ自身に変換され、コンビネータ項において許されている適用は単にアプリカンドとコンビネータへの引数の変換である。
5番目と6番目の規則は興味深い。5番目は複雑な抽象をコンビネータに変換することを単純に示している。まず本体をコンビネータに変換し、それから抽象を除去する。6番目は実際に抽象を除去する。
λx.(E₁ E₂)はaという引数を取り、ラムダ項(E₁ E₂)のxを置き換えて (E₁ E₂)[x : = a]を生成する関数である。
しかし、(E₁ E₂)の中のxをaで置き換えるのはちょうどE₁ and E₂を置き換えるのと同じである。だから
       (E₁ E₂)[x := a] = (E₁[x := a] E₂[x := a])
       (λx.(E₁ E₂) a) = ((λx.E₁ a) (λx.E₂ a))
                      = (S λx.E₁ λx.E₂ a)
                      = ((S λx.E₁ λx.E₂) a)
外延的同値性によって、
       λx.(E₁ E2)     = (S λx.E₁ λx.E₂)
したがって、λx.(E₁ E₂)と等しいコンビネータを見つけるには、(S λx.E₁ λx.E₂)と等しいコンビネータを探せば十分である。そして
       (S T[λx.E₁] T[λx.E₂])
は明らかにその要件に適合する。E₁とE₂がそれぞれ(E₁ E₂)より厳密に少ない適用を含むため、再帰はすべての変数及びλx.Eの形の項において終了させなければならない。

η-簡約

T[ ]変換によって生成されたコンビネータはη-reductionによって小さくなりうる。
       T[λx.(E x)] = T[E]   (if x is not free in E)
λx.(E x)はxを引数にとり、Eを適用する関数である。それは外延的にはE自身と同値である。それはつまりEをコンビネータの形にすれば十分である。
この例は、この簡略化を根拠付ける。
         T[λx.λy.(y x)]
       = ...
       = (S (K (S I))   T[λx.(K x)])
       = (S (K (S I))   K)                 (by η-reduction)
このコンビネータはより早く、長いものと同値である。
         (S (K (S I))   K x y)
       = (K (S I) x (K x) y)
       = (S I (K x) y)
       = (I y (K x y))
       = (y (K x y))
       = (y x)
同様に、もとのT[ ]はλf.λx.(f x)を(S (S (K S) (S (K K) I)) (K I))に変換したが、η-簡約を用いればλf.λx.(f x)はIに変換される。

One-point basis

すべてのコンビネータがすべてのラムダ項と外延的に等しくなるようなone-point basesが存在する。そのような基底のもっとも単純な例Xはこうである。
       X ≡ λx.((xS)K)
それを確かめるのは難しくない。
       X (X (X X)) =ηβ K and
       X (X (X (X X))) =ηβ S.
{K, S}が基底だから、{X}もまた基底である。プログラミング言語IotaはXをその唯一のコンビネータとして使う。
one-point basisのもう一つの簡単な例は
       X' ≡ λx.(x K S K) with
       (X' X') X' =β K and
       X' (X' X') =β S
X' はKとSを生成するのにη変換を必要としない。

逆変換

コンビネータの項からラムダ項への変換L[ ]は自明である。
       L[I]       = λx.x
       L[K]       = λx.λy.x
       L[C]       = λx.λy.λz.(x z y)
       L[B]       = λx.λy.λz.(x (y z))
       L[S]       = λx.λy.λz.(x z (y z))
       L[(E₁ E₂)] = (L[E₁] L[E₂])
これは、前述のT[ ]の逆変換ではないことに注意。

関数型言語のコンパイル

関数型言語は、ラムダ計算がシンプルながら万能性があるため、ラムダ計算をベースとしているものが多いが、ラムダ式はコンビネータ式に変換可能であり、一種のコンパイルとも言える。David Turnerは、SASLの実装にコンビネータを利用した（SASLに限らず、一般に関数型言語の実装に応用可能である）。
Kenneth E. Iversonは、APLの後続に位置づけられるJ (プログラミング言語)で、カリーのコンビネータを基本としたプリミティブを採用し、Iversonがtacit programming（en:Tacit programming）と呼んだものを可能にした。それは、変数を含まない式で、そのようなプログラムで作業するための強力なツールに沿って行うプログラミングである。APLのような言語では、ユーザー定義の演算子を用いたclumsier mannerで暗黙のプログラミングが可能であることが判明した。(Pure Functions in APL and J)