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

コンビネータ論理は、コンビネータまたは引数のみからなる関数適用によって結果が定義されている高階関数、コンビネータに基づいている。
数学におけるコンビネータ論理

コンビネータ論理は元来、本質的に量化変数を消去することによって量化変数の役割を明確にするような「pre-logic」を意図していた。量化変数を消去する方法にはクワインの述語関手論理がある。コンビネータ論理の表現力は一階述語論理を超える一方、述語関手論理の表現力は一階述語論理と同等である。

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

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

計算機科学において（計算可能性理論や証明論で）は、コンビネータ論理は計算を単純化したモデルとして使われる。単純にもかかわらず、コンビネータ論理は計算の本質的な特徴をとらえている。

コンビネータ論理はラムダ計算の変種としても見ることができる。ラムダ式(ラムダ抽象)は、束縛変数のない原始的な関数「コンビネータ」の有限集合によって置き換えられる。ラムダ式をコンビネータ式に変換するのは簡単であり、またコンビネータの簡約はラムダの簡約よりもシンプルである。したがってコンビネータ論理は非正格関数型言語やGraph reduction machineのモデルとして使われている。もっとも純粋な形は、唯一のプリミティブが入出力のために拡張されたSとKのコンビネータの、Unlambdaというプログラミング言語である。実用的なプログラミング言語ではないが、Unlambdaは理論的な関心がある。

コンビネータ論理は解釈の多様性を与えられる。カリーによる論文では、どのように従来の論理のための公理をコンビネータ論理の等式にするかを示した。デイナ・スコットは、60,70年代にどのようにしてモデル理論とコンビネータ論理を結びつけるかを示した。
ラムダ計算の概要詳細は「ラムダ計算」を参照

ラムダ計算は、ラムダ項と呼ばれる以下のような形の記号の列に関係している。

v

λv.E1

(E1 E2)

vは予め定義された変数の名前の無限集合から引き出された変数名で、E1とE2はラムダ項である。λv.E1の形の項は「抽象」と呼ばれる。vはその抽象の仮引数、E1は本体と呼ばれる。λv.E1という項は、引数に適用されるとvをその値に束縛し、E1の結果の値を評価する。つまり、E1の中にあるvをその引数で置き換えたものを返す。(E1 E2)の形の項は適用と呼ばれる。適用は関数の呼び出しもしくは実行を作る:E1という関数が、E2という引数で呼び出されると、その結果が計算される。もしE1(ときどきapplicandと呼ばれる)がラムダ抽象なら、その項は簡約されるかもしれない: 引数E2は、E1の仮引数の場所に置き換えられ、同値な新しい項が結果になる。もし、ラムダ項が((λv.E1) E2)の形の項を含まないのならば、それは簡約されず、β正規形と呼ばれる。E[v := a]は、Eのvの自由変数としての出現をすべてaで置き換えた結果を表現する。したがって、((λv.E)a) => E[v := a]

伝統的に、(a b c d ... z)を(...(((a b) c) d) ... z)の省略として表記する。(i.e. 適用は左結合である)このような定義をするのは、すべての数学的の根本的な振る舞いを捉えているからである。例えば、ある数の平方を求める関数を考えて欲しい。英語ならこのように書くかもしれない。The square of x is x*x

(「*」を乗算の表記に用いている。) xは関数の仮引数である。特定の引数の平方を求めるために、3をあてると、仮引数の場所に3を入れる:The square of 3 is 3*3

3*3の結果を求めるためには、乗算と3という数の知識に頼らなければならない。あらゆる計算は、単に適切な関数と適切な原始的な引数の評価の合成だから、この単純な置き換えの原理は、計算の本質的なメカニズムを捉えるには十分である。さらに、ラムダ計算では3や*は外部の演算子や定数をまったく使わずに表現されうる。ラムダ計算では、適切に解釈された時3や乗算演算子のように振る舞う項を識別することが可能である。(チャーチエンコーディングを参照)ラムダ計算は、計算としてほかのもっともらしい計算のモデル(チューリングマシンを含む)と同等の力があることが分かっている。つまり、あらゆる計算を行える他のモデルはラムダ計算で表現でき、逆もそうである。チャーチ・チューリングのテーゼによれば、両方のモデルはあらゆる可能な計算を表現できる。すべての計算が、ラムダ抽象と適用を基本とした変数の置き換えのシンプルな概念で表現できることは、おそらく驚くべきことである。しかし、さらに目覚ましいのは、ラムダ抽象も必要がないことである。コンビネータ論理はラムダ計算と同等のモデルだが、ラムダ抽象は存在しない。ラムダ計算での式の評価は非常に複雑である(置換の意味論は変数を捉えるのを避けるためのかなりの気配りと共に決めなければならない)。対照的に、コンビネータ論理の式の評価は置換という概念が存在しないため、はるかに簡単である。
コンビネータ計算

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