コンビネータ論理
コンビネータ論理(Combinatory Logic、組み合わせ論理)は、（、）とハスケル・カリー（）によって、記号論理での変数を消去するために導入された記法である。最近では、計算機科学において計算の理論的モデルで利用されてきている。また、関数型プログラミング言語の理論（意味論など）や実装にも応用がある。
コンビネータ論理は、コンビネータまたは引数のみからなる関数適用によって結果が定義されている高階関数、コンビネータに基づいている。
コンビネータ論理は元来、本質的に量化変数を消去することによって量化変数の役割を明確にするような「pre-logic」を意図していた。量化変数を消去する方法にはクワインの述語関手論理がある。コンビネータ論理の表現力は一階述語論理を超える一方、述語関手論理の表現力は一階述語論理と同等である。
コンビネータ論理の最初の発明者であるは、1924年の論文以降それについて何も出版していない（ヨシフ・スターリンが1929年に権力を確固なものとしてからはほとんど出版を行なっていない）。1927年後半、カリーはプリンストン大学の講師として働いているときにコンビネータを再発見した。1930年代後半、アロンゾ・チャーチとプリンストン大学の彼の教え子が、ラムダ計算というライバルとなる関数抽象の形式化を考案し、コンビネータ論理より人気を博すこととなった。こうした歴史的偶然のために、理論計算機科学が60〜70年代にコンビネータ論理に関心を持ち始めるまで、この分野のほとんどすべての業績は、ほとんどカリーとその教え子、もしくはベルギーのによるものであった。Curry and Feys (1958) および Curry et al. (1972) はコンビネータ論理の初期の歴史についてのサーベイ論文である。より最近のコンビネータ論理とラムダ計算の比較については (1984) を参照されたい（デイナ・スコットが60〜70年代に考案したコンビネータ論理のためのモデル理論についても触れている）。
計算機科学において（計算可能性理論や証明論で）は、コンビネータ論理は計算を単純化したモデルとして使われる。単純にもかかわらず、コンビネータ論理は計算の本質的な特徴をとらえている。
コンビネータ論理はラムダ計算の変種としても見ることができる。ラムダ式(ラムダ抽象)は、束縛変数のない原始的な関数「コンビネータ」の有限集合によって置き換えられる。ラムダ式をコンビネータ式に変換するのは簡単であり、またコンビネータの簡約はラムダの簡約よりもシンプルである。したがってコンビネータ論理は非正格関数型言語やGraph reduction machineのモデルとして使われている。もっとも純粋な形は、唯一のプリミティブが入出力のために拡張されたSとKのコンビネータの、Unlambdaというプログラミング言語である。実用的なプログラミング言語ではないが、Unlambdaは理論的な関心がある。
コンビネータ論理は解釈の多様性を与えられる。カリーによる論文では、どのように従来の論理のための公理をコンビネータ論理の等式にするかを示した。デイナ・スコットは、60,70年代にどのようにしてモデル理論とコンビネータ論理を結びつけるかを示した。
ラムダ計算は、ラムダ項と呼ばれる以下のような形の記号の列に関係している。"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"で置き換えた結果を表現する。したがって、
伝統的に、"(a b c d ... z)"を"(...(((a b) c) d) ... z)"の省略として表記する。(i.e. 適用は左結合である)
このような定義をするのは、すべての数学的の根本的な振る舞いを捉えているからである。例えば、ある数の平方を求める関数を考えて欲しい。英語ならこのように書くかもしれない。
(「*」を乗算の表記に用いている。) "x"は関数の仮引数である。特定の引数の平方を求めるために、3をあてると、仮引数の場所に3を入れる:
3*3の結果を求めるためには、乗算と3という数の知識に頼らなければならない。あらゆる計算は、単に適切な関数と適切な原始的な引数の評価の合成だから、この単純な置き換えの原理は、計算の本質的なメカニズムを捉えるには十分である。さらに、ラムダ計算では"3"や"*"は外部の演算子や定数をまったく使わずに表現されうる。ラムダ計算では、適切に解釈された時3や乗算演算子のように振る舞う項を識別することが可能である。(チャーチエンコーディングを参照)
ラムダ計算は、計算としてほかのもっともらしい計算のモデル(チューリングマシンを含む)と同等の力があることが分かっている。つまり、あらゆる計算を行える他のモデルはラムダ計算で表現でき、逆もそうである。チャーチ・チューリングのテーゼによれば、両方のモデルはあらゆる可能な計算を表現できる。
すべての計算が、ラムダ抽象と適用を基本とした変数の置き換えのシンプルな概念で表現できることは、おそらく驚くべきことである。
しかし、さらに目覚ましいのは、ラムダ抽象も必要がないことである。"コンビネータ論理"はラムダ計算と同等のモデルだが、ラムダ抽象は存在しない。ラムダ計算での式の評価は非常に複雑である(置換の意味論は変数を捉えるのを避けるためのかなりの気配りと共に決めなければならない)。対照的に、コンビネータ論理の式の評価は置換という概念が存在しないため、はるかに簡単である。
ラムダ抽象が関数を作るための唯一の方法だから、コンビネータ計算の中では何かがそれを置き換えねばならない。コンビネータ計算は、ラムダ抽象の代わりに、原始的な関数の有限集合を提供する。
コンビネータ項は以下の形式のうち一つを持つ:
"x"は変数、"P"は原始的関数、("E" "E") は項の適用である。原始的関数はコンビネータ、もしくは、自由変数を含まないラムダ項である。
表記を短縮するために、伝統的に("E" "E" "E" ... "E")ないし"E" "E" "E" ... "E"は(...(("E" "E") "E")..."E")を示す。
コンビネータ論理では、それぞれの原始的なコンビネータは以下のような形の簡約のルールを持つ。
"E"は"x" ..."x"の項のみに言及している項で、原始的なコンビネータが関数として振る舞う方法にある。
もっとも単純なコンビネータの例は、以下のように定義される恒等コンビネータIである。
もうひとつの単純なコンビネータはKで、定数関数を作る。(K "x")はどんな引数に対しても"x"を返す関数である。そして、Kはこのように定義する:
もしくは、伝統的な複数の適用の表記に従えば
三つ目のコンビネータは、適用を一般化したSである。
Sは、それぞれに"z"を適用したあと"x"を"y"に適用する。別の言い方をすれば、zという環境において"x"を"y"に適用する。
S and Kがあれば、Iは不必要である。なぜなら、他の二つでこのようにして表現できるからである。
すべての項"x"に対して((S K K) "x") = (I "x")が成り立つが、(S K K)自身はIとは同じではない。これらの項は外延的に同値である。外延的同値は"関数の同値"という数学的な概念である。二つの関数が、同じ引数に対して常に同じ結果を返すならばそれは"等しい"。対照的に、原始的なコンビネータと一緒にあるそれらの項自身は、"内包的同値"という概念を捉える。十分な引数が与えられたときに、原始的なコンビネータに展開されるまで同じ形をもつ時だけ、それらは同値である。
恒等関数を実装するにはたくさんの方法がある。(S K K)とIはそれに含まれている。さらに、(S K S)もそうである。今後、"同値"という言葉を外延的同値を示し、"等しい"を同じコンビネータを示すのに使う。
さらに面白いコンビネータは、再帰を実装するために使える不動点コンビネータ(Yコンビネータ)である。
SとKが外延的にすべてのラムダ項と同値なものに合成されうるのは、おそらく驚くべき事実である。したがって、チャーチのテーゼによれば、それはあらゆる計算可能な関数に合成されうる。その証明は、"T"[ ]という任意のラムダ項を同値なコンビネータにする変換を示すことで与えられる。
"T"[ ]は以下のように定義する。これは"abstraction elimination"として知られている。
たとえば、"λx"."λy".("y" "x")をコンビネータにしてみよう。
任意の二つの項"x"と"y"をこのコンビネータに合成すると、以下のように簡約される。
(S (K (S I)) (S (K K) I))という表現は、ラムダ項としての表現"λx"."λy".(y x)よりもはるかに長い。これは一般的なことである。普通、"T"[ ]はラムダ項をΘ("n")に展開する。
Tは抽象を消去することが動機となっている。規則3、4は自明である:"λx"."x"は明らかにIと等しく、"λx"."E"はxが自由変数としてEに出現しない時明らかに(K"T"["E"])である。
最初の二つの規則も単純である。変数はそれ自身に変換され、コンビネータ項において許されている適用は単にアプリカンドとコンビネータへの引数の変換である。
5番目と6番目の規則は興味深い。5番目は複雑な抽象をコンビネータに変換することを単純に示している。まず本体をコンビネータに変換し、それから抽象を除去する。6番目は実際に抽象を除去する。
"λx".("E₁" "E₂")はaという引数を取り、ラムダ項("E₁" "E₂")のxを置き換えて ("E₁" "E₂")["x" : = "a"]を生成する関数である。
しかし、("E₁" "E₂")の中の"x"を"a"で置き換えるのはちょうど"E₁" and "E₂"を置き換えるのと同じである。だから
外延的同値性によって、
したがって、"λx".("E₁" "E₂")と等しいコンビネータを見つけるには、(S "λx"."E₁" "λx"."E₂")と等しいコンビネータを探せば十分である。そして
は明らかにその要件に適合する。"E₁"と"E₂"がそれぞれ("E₁" "E₂")より厳密に少ない適用を含むため、再帰はすべての変数及び"λx"."E"の形の項において終了させなければならない。
"T"[ ]変換によって生成されたコンビネータは"η-reduction"によって小さくなりうる。
"λx".("E" x)はxを引数にとり、"E"を適用する関数である。それは外延的には"E"自身と同値である。それはつまり"E"をコンビネータの形にすれば十分である。
この例は、この簡略化を根拠付ける。
このコンビネータはより早く、長いものと同値である。
同様に、もとの"T"[ ]は"λf"."λx".("f" "x")を(S (S (K S) (S (K K) I)) (K I))に変換したが、η-簡約を用いれば"λf"."λx".("f" "x")はIに変換される。
すべてのコンビネータがすべてのラムダ項と外延的に等しくなるようなone-point basesが存在する。そのような基底のもっとも単純な例Xはこうである。
それを確かめるのは難しくない。
one-point basisのもう一つの簡単な例は
X' はKとSを生成するのにη変換を必要としない。
SとKに加え、の論文ではBとCと呼ばれる、以下のような簡約をするコンビネータを含めた。
彼は、どのようにしてSとKだけを用いてこれらを表現できるかを説明した。
これらのコンビネータは述語論理やラムダ計算をコンビネータ式にする際に非常に有用である。これらはハスケル・カリーと、だいぶ後に計算機における用法と関連付けたデビッド・ターナーによって使われた。これらを使って、以下のように変換のルールを拡張できる。BとCコンビネータを使うと、"λx"."λy".("y" "x")の変換はこのようになる。
確かに、(C I "x" "y")は("y" "x")に簡約される。
その動機は、BとCは限定されたSであるということである。
Sは値を取り両方のアプリカンドを置き換えて適用を行う一方。Cはアプリカンドのみ、Bは引数のみを置き換える。
そのコンビネータのための近代的な名前は、ハスケル・カリーの1930年の博士論文による(B,C,K,Wシステムを参照)。のもとの論文では、今S, K, I, B,Cと呼んでいるものはそれぞれS, C, I, Z, Tと呼ばれていた。
新しい変換の規則によるコンビネータのサイズの短縮はBとCを用いなくても、この論文の節3.2のように達成できる。
この記事で述べているCL算法とCL算法は区別されなければならない。これらの区別は、λとλ算法に対応する。λ算法と違い、λ算法は抽象を以下のように制限する。
結果として、KはλにもCLにも与えられない。CLの定数は、I, B, C,Sであり、CLのすべての項が合成される。λからCLへの変換と似たようなルールに合わせ、すべてのλの項は、等しいCLに変換される。Barendregt (1984)の第9章を参照されたい。
コンビネータの項からラムダ項への変換"L"[ ]は自明である。
これは、前述の"T"[ ]の逆変換ではないことに注意。
一般的なコンビネータ項が正規形を持つかどうか、二つのコンビネータ項が同じかどうかは判定できない。これは、対応するラムダ項における非決定性と同じである。直接的な証明は以下のようになる。
まず、以下の項を見てみよう。
この項は正規形を持たない。なぜなら、以下に示すようにこれは自分自身に簡約するからである。
そして、明らかにこれ以上短い式を作る簡約はない。
正規形を検出するコンビネータNを考えてみよう。
(S I I "Z")という項を考えてみよう。(S I I "Z")は正規形を持つだろうか？それはもししこのようにしたとき、そうである。
今、Nを(S I I "Z")に適用する必要がある。
(S I I "Z")が正規形を持つか、そうでないか。もしそれが正規形を"持つ"ならば、以下のように簡約される。
しかし、Ωは正規形を持たないため、矛盾している。もし、(S I I "Z")が正規形を"持たない"ならば、このように簡約する。
(S I I "Z")の正規形は単にIであり、また矛盾を生む。したがって、仮定した正規形コンビネータNは存在できない。
ライスの定理におけるコンビネータ論理の例(原文：The combinatory logic analogue)が言うのは、完全で非自明な述語は存在しないという事である。ある述語がコンビネータであるということは、適用の際にTrueかFalseのどちらかを返すということである。もし2つの"NA"=Tと"NB"=Fを満たすような2つの引数"A","B"が存在するとき、その述語"N"は非自明であるという。また、"NM"がいかなる引数"M"についても正規形をしているとき、そしてその時に限り述語"N"が完全であるという。ライスの定理の例は、全ての完全な述語は自明であると述べている。この定理の証明はかなり単純である。
証明:背理法による。完全で非自明な述語の存在を仮定し、N と呼ぶことにする。
Nは非自明であるから以下を満たすコンビネータA,Bが存在する。
("N A") = T
("N B") = F
Define NEGATION ≡ "λx."(if ("N x") then "B" else "A") ≡ "λx."(("N x") "B" "A")
Define ABSURDUM ≡ (Y NEGATION)
不動点定理により、
ABSURDUM ≡ (Y NEGATION) = (NEGATION (Y NEGATION)) ≡ (NEGATION ABSURDUM)
を満たすABSURDUM = (NEGATION ABSURDUM)が与えられる。
Nは完全であるから以下の2つのうちどちらかを満たす。
場合1: F = F = ("N" ABSURDUM) = "N" (NEGATION ABSURDUM) = ("N A") = T これは矛盾である。
場合2: T = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N B) = F これもまた矛盾である。
故に、 ("N" ABSURDUM) は真であっても偽であってもNが完全で非自明な述語であることに反する。QED。
この論証不明の定理からすぐに、正規形をもつ条件を満たすかどうかを決定することができる完全な述語は存在しないことが導かれる。さらに、
(EQUAL "A B") = T if "A" = "B" and
(EQUAL "A B") = F if "A" ≠ "B".
でのEQUALのような完全な述語は存在しないことも言える。
もしもEQUALが存在したならば、全てのAについて λx.(EQUAL x A) は完全で非自明な述語でなければならない。
この結果はコンビネータ論理の決定不能性を意味しないことに注意しなければならない。これらの結果のいうところは、コンビネータそれ自身を引数に取り（ある条件を満たす）性質を判定するコンビネータが存在しないということであり、計算論的な意味の不能性を意味するわけではない。実際、コンビネータの構文的な等価性は上の定理によればコンビネータにより判定することはできない（コンビネータ論理の定義には異なる変数記号を体系内で区別するような規則は何一つとして含まれてはいない）が、明らかに計算可能である。コンビネータ論理の決定不能性を示すには、コンビネータをゲーデル数を用いて自然数にコーディングの上で、ゲーデル数を表すコンビネータを引数に取り（ある条件を満たす）性質を判定するコンビネータが存在しないということを証明すればよい。一般に、非自明かつweak同値性に関して閉じたn-項関係は決定不能である。それゆえ、上述したような述語は、ゲーデル数を用いてもなお表現できない。その証明は最初に述べた証明を多少変更するだけで得られる。一方で、あるゲーデル数に対してコンビネータの構文的な等価性を判定するコンビネータを構成することもできる。
関数型言語は、ラムダ計算がシンプルながら万能性があるため、ラムダ計算をベースとしているものが多いが、ラムダ式はコンビネータ式に変換可能であり、一種のコンパイルとも言える。David Turnerは、SASLの実装にコンビネータを利用した（SASLに限らず、一般に関数型言語の実装に応用可能である）。
Kenneth E. Iversonは、APLの後続に位置づけられるJ (プログラミング言語)で、カリーのコンビネータを基本としたプリミティブを採用し、Iversonがtacit programming（）と呼んだものを可能にした。それは、変数を含まない式で、そのようなプログラムで作業するための強力なツールに沿って行うプログラミングである。APLのような言語では、ユーザー定義の演算子を用いたclumsier mannerで暗黙のプログラミングが可能であることが判明した。(Pure Functions in APL and J)
カリー＝ハワード同型対応によれば、論理式と型が対応し、直観主義論理の含意断片のヒルベルト流の推論図と型付きコンビネータ項が対応する。
コンビネータK、Sは以下の公理型に対応する。
そして、関数適用はモーダスポネンスに対応する。
コンビネータ項に直和や直積の為の定数を加え、さらに基本型としてbottom formula_1、複合型として直積型と直和型を加えたものは、ヒルベルト流の直観主義命題論理と対応する。