コンビネータ論理

コンビネータ論理（英: combinatory logic、組み合わせ論理）は、モイセイ・シェインフィンケリ（ロシア語版、英語版）（露: Моисей Эльевич Шейнфинкель、英: Moses Ilyich Schönfinkel）とハスケル・カリー（英: 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や乗算演算子のように振る舞う項を識別することが可能である。(チャーチエンコーディングを参照) ラムダ計算は、計算としてほかのもっともらしい計算のモデル(チューリングマシンを含む)と同等の力があることが分かっている。つまり、あらゆる計算を行える他のモデルはラムダ計算で表現でき、逆もそうである。チャーチ・チューリングのテーゼによれば、両方のモデルはあらゆる可能な計算を表現できる。すべての計算が、ラムダ抽象と適用を基本とした変数の置き換えのシンプルな概念で表現できることは、おそらく驚くべきことである。しかし、さらに目覚ましいのは、ラムダ抽象も必要がないことである。コンビネータ論理はラムダ計算と同等のモデルだが、ラムダ抽象は存在しない。ラムダ計算での式の評価は非常に複雑である(置換の意味論は変数を捉えるのを避けるためのかなりの気配りと共に決めなければならない)。対照的に、コンビネータ論理の式の評価は置換という概念が存在しないため、はるかに簡単である。

コンビネータ計算

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

コンビネータ項

コンビネータ項は以下の形式のうち一つを持つ:

x
P
(E₁ E₂)

xは変数、Pは原始的関数、(E₁ E₂) は項の適用である。原始的関数はコンビネータ、つまり、ラムダ項として見たときには自由変数を持たない関数である。

表記を短縮するために、伝統的に(E₁ E₂ E₃ ... E_n)ないしE₁ E₂ E₃ ... E_nは(...((E₁ E₂) E₃)...E_n)を示す。

コンビネータ論理での簡約

コンビネータ論理では、それぞれの原始的コンビネータは以下のような形の簡約のルールを持つ。

(P x₁ ... x_n) = E

Eは変数x₁ ...x_nのみに言及している項である。これらのルールは、原始的コンビネータが関数として振る舞う方法を定義している。

コンビネータの例

もっとも単純なコンビネータの例は、以下のように定義される恒等コンビネータ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コンビネータ)である。

S-K basisの完全性

SとKが外延的にすべてのラムダ項と同値なものに合成されうるのは、おそらく驚くべき事実である。したがって、チャーチのテーゼによれば、それはあらゆる計算可能な関数に合成されうる。その証明は、T[ ]という任意のラムダ項を同値なコンビネータにする変換を示すことで与えられる。 T[ ]は以下のように定義する。

T[x] => x
T[(E₁ E₂)] => (T[E₁] T[E₂])
T[λx.E] => (K T[E]) (if x does not occur free in E)
T[λx.x] => I
T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E)
T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])

これはabstraction eliminationとして知られている。

ラムダ抽象から同値なcombinatorial termへの変換

たとえば、λx.λy.(y x)をコンビネータにしてみよう。

T[λx.λy.(y x)]

= T[λx.T[λy.(y x)]] (by 5)

= T[λx.(S T[λy.y] T[λy.x])] (by 6)

= T[λx.(S I T[λy.x])] (by 4)

= T[λx.(S I (K x))] (by 3 and 1)

= (S T[λx.(S I)] T[λx.(K x)]) (by 6)

= (S (K (S I)) T[λx.(K x)]) (by 3)

= (S (K (S I)) (S T[λx.K] T[λx.x])) (by 6)

= (S (K (S I)) (S (K K) T[λx.x])) (by 3)

= (S (K (S I)) (S (K K) I)) (by 4)

任意の二つの項xとyをこのコンビネータに合成すると、以下のように簡約される。

(S (K (S I)) (S (K K) I) x y)

= (K (S I) x (S (K K) I x) y)

= (S I (S (K K) I x) y)

= (I y (S (K K) I x y))

= (y (S (K K) I x y))

= (y (K K x (I x) y))

= (y (K (I x) y))

= (y (I x))

= (y x)

(S (K (S I)) (S (K K) I))という表現は、ラムダ項としての表現λx.λy.(y x)よりもはるかに長い。これは一般的なことである。普通、T[ ]はラムダ項をΘ(n²)に展開する。

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を生成するのにη変換を必要としない。

B,Cコンビネータ

SとKに加え、モイセイ・シェインフィンケリ（ロシア語版、英語版）の論文ではBとCと呼ばれる、以下のような簡約をするコンビネータを含めた。

       (C f x y) = (f y x)
       (B f g x) = (f (g x))

彼は、どのようにしてSとKだけを用いてこれらを表現できるかを説明した。これらのコンビネータは述語論理やラムダ計算をコンビネータ式にする際に非常に有用である。これらはハスケル・カリーと、だいぶ後に計算機における用法と関連付けたデビッド・ターナーによって使われた。これらを使って、以下のように変換のルールを拡張できる。

T[x] => x
T[(E₁ E₂)] => (T[E₁] T[E₂])
T[λx.E] => (K T[E]) (if x is not free in E)
T[λx.x] => I
T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E)
T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂]) (if x is free in both E₁ and E₂)
T[λx.(E₁ E₂)] => (C T[λx.E₁] T[E₂]) (if x is free in E₁ but not E₂)
T[λx.(E₁ E₂)] => (B T[E₁] T[λx.E₂]) (if x is free in E₂ but not E₁)

BとCコンビネータを使うと、λx.λy.(y x)の変換はこのようになる。

         T[λx.λy.(y x)]
       = T[λx.T[λy.(y x)]]
       = T[λx.(C T[λy.y] x)]     (by rule 7)
       = T[λx.(C I x)]
       = (C I)                   (η-reduction)
       = C_*(traditional canonical notation : X_* = X I)
       = I'(traditional canonical notation: X' = C X)

確かに、(C I x y)は(y x)に簡約される。

         (C I x y)
       = (I y x)
       = (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を用いなくても、この論文^[2]の節3.2のように達成できる。

CL_KとCL_I算法

この記事で述べているCL_K算法とCL_I算法は区別されなければならない。これらの区別は、λ_Kとλ_I算法に対応する。λ_K算法と違い、λ_I算法は抽象を以下のように制限する。

λx.E where x has at least one free occurrence in E.

λx.Eにおいて、xはEの中で少なくとも一つは自由に出現している。

結果として、Kはλ_IにもCL_Iにも与えられない。CL_Iの定数は、I, B, C,Sであり、CL_Iのすべての項が合成される。λ_KからCL_Kへの変換と似たようなルールに合わせ、すべてのλ_Iの項は、等しいCL_Iに変換される。Barendregt (1984)の第9章を参照されたい。

逆変換

コンビネータの項からラムダ項への変換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[ ]の逆変換ではないことに注意。

コンビネータ計算の非決定性

一般的なコンビネータ項が正規形を持つかどうか、二つのコンビネータ項が同じかどうかは判定できない。これは、対応するラムダ項における非決定性と同じである。直接的な証明は以下のようになる。まず、以下の項を見てみよう。

       Ω = (S I I (S I I))

この項は正規形を持たない。なぜなら、以下に示すようにこれは自分自身に簡約するからである。

         (S I I (S I I))
       = (I (S I I) (I (S I I)))
       = (S I I (I (S I I)))
       = (S I I (S I I))

そして、明らかにこれ以上短い式を作る簡約はない。正規形を検出するコンビネータNを考えてみよう。

       (N x) => T, if x has a normal form
                F, otherwise.

(TとFはチャーチエンコーディングにおける真理値を表現する。λx.λy.xとλx.λy.yで、コンビネータの形ではT = K and F = (K I)である。) そして、

       Z = (C (C (B N (S I I)) Ω) I)

(S I I Z)という項を考えてみよう。(S I I Z)は正規形を持つだろうか？それはもしこのようにしたとき、こうなる。

         (S I I Z)
       = (I Z (I Z))
       = (Z (I Z))
       = (Z Z)
       = (C (C (B N (S I I)) Ω) I Z)           (definition of Z)
       = (C (B N (S I I)) Ω Z I)
       = (B N (S I I) Z Ω I)
       = (N (S I I Z) Ω I)

今、Nを(S I I Z)に適用する必要がある。 (S I I Z)が正規形を持つか、そうでないか。もしそれが正規形を持つならば、以下のように簡約される。

         (N (S I I Z) Ω I)
       = (K Ω I)                               (definition of N)
       = Ω

しかし、Ωは正規形を持たないため、矛盾している。もし、(S I I Z)が正規形を持たないならば、このように簡約する。

         (N (S I I Z) Ω I)
       = (K I Ω I)                             (definition of N)
       = (I I)
         I

(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つのうちどちらかを満たす。

(N ABSURDUM) = F
(N ABSURDUM) = T

場合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（en:Tacit programming）と呼んだものを可能にした。それは、変数を含まない式で、そのようなプログラムで作業するための強力なツールに沿って行うプログラミングである。APLのような言語では、ユーザー定義の演算子を用いたclumsier mannerで暗黙のプログラミングが可能であることが判明した。(Pure Functions in APL and J)

論理学

カリー＝ハワード同型対応によれば、論理式と型が対応し、直観主義論理の含意断片のヒルベルト流の推論図と型付きコンビネータ項が対応する。コンビネータK、Sは以下の公理図式に対応する。

AK: A → (B → A),

AS: (A → (B → C)) → ((A → B) → (A → C)),

そして、関数適用はモーダスポネンスに対応する。

MP: A と A → B から B を推論できる。

コンビネータ項に直和や直積の為の定数を加え、さらに基本型としてbottom $\bot$ 、複合型として直積型と直和型を加えたものは、ヒルベルト流の直観主義命題論理と対応する。

脚注

^ Seldin, Jonathan. The Logic of Curry and Church.
^ John Tromp, Binary Lambda Calculus and Combinatory Logic, in Randomness And Complexity, from Leibniz To Chaitin, ed. Cristian S. Calude, World Scientific Publishing Company, October 2008. (pdf version)

参考文献

Hendrik Pieter Barendregt, 1984. The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, Volume 103, North-Holland.ISBN 0-444-87508-5
Curry, Haskell B.; Feys, Robert (1958). Combinatory Logic. Vol. I. Amsterdam: North Holland. ISBN 0-7204-2208-6
Curry, Haskell B.; Hindley, J. Roger; Seldin, Jonathan P. (1972). Combinatory Logic. Vol. II. Amsterdam: North Holland. ISBN 0-7204-2208-6
Field, Anthony J. and Peter G. Harrison, 1998. Functional Programming. . Addison-Wesley. ISBN 0-201-19249-7
Hindley, J. Roger; Meredith, David (1990), “Principal type-schemes and condensed detachment”, Journal of Symbolic Logic 55 (1): 90–105, MR1043546
Hindley, J. R., and Seldin, J. P. (2008) λ-calculus and Combinators: An Introduction. Cambridge Univ. Press.
Paulson, Lawrence C., 1995. Foundations of Functional Programming. University of Cambridge.
Quine, W. V., 1960 "Variables explained away", Proceedings of the American Philosophical Society 104:3:343–347 (June 15, 1960) at JSTOR. Reprinted as Chapter 23 of Quine's Selected Logic Papers(1966), pp. 227–235
Moses Schönfinkel, 1924, "Über die Bausteine der mathematischen Logik," translated as "On the Building Blocks of Mathematical Logic" in From Frege to Gödel: a source book in mathematical logic, 1879–1931, Jean van Heijenoort, ed. Harvard University Press, 1967. ISBN 0-674-32449-8. The article that founded combinatory logic.
Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. Lectures on the Curry–Howard Isomorphism. University of Copenhagen and University of Warsaw, 1999.
Smullyan, Raymond, 1985. To Mock a Mockingbird. Knopf. ISBN 0-394-53491-3. A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors.
- スマリヤン『ものまね鳥をまねる』（POD版 http://www.morikita.co.jp/books/book/142 、 http://www.morikita.co.jp/books/book/141 ）
--------, 1994. Diagonalization and Self-Reference. Oxford Univ. Press. Chpts. 17-20 are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.
Wolfengagen, V.E. Combinatory logic in programming. Computations with objects through examples and exercises. -- 2-nd ed. -- M.: "Center JurInfoR" Ltd., 2003. -- x+337 с. ISBN 5-89158-101-9.

外部リンク

Stanford Encyclopedia of Philosophy: "Combinatory Logic" by Katalin Bimbó.
1920–1931 Curry's block notes.
Keenan, David C. (2001) "To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction."
Rathman, Chris, "Combinator Birds." A table distilling much of the essence of Smullyan (1985).
Drag 'n' Drop Combinators. (Java Applet)
Binary Lambda Calculus and Combinatory Logic.
Combinatory logic reduction web server

[Seldin_2006-1] Seldin, Jonathan. The Logic of Curry and Church.

[2] John Tromp, Binary Lambda Calculus and Combinatory Logic, in Randomness And Complexity, from Leibniz To Chaitin, ed. Cristian S. Calude, World Scientific Publishing Company, October 2008. (pdf version)

[1]

[2]

典拠管理データベース
国立図書館	フランス BnF data ドイツイスラエルアメリカ
その他	IdRef