利用者:Fumiexcel/Combinatory logic

コンビネータ論理(Combinatory Logic)は、Moses Schönfinkelとハスケル・カリーによって、記号論理での変数を消去するために導入された記法である。最近では、計算機科学において計算の理論的モデルで利用されてきている。また、関数型プログラミング言語の基礎にもなっている。

コンビネータ論理は、関数適用と、引数に対する結界を定義したコンビネータだけを用いる高階関数、コンビネータに基づいている。

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

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

combinatory logicの最初の発明者であるMoses Schönfinkelは、彼の1924年の論文以降それについて何も公開せす、ヨシフ・スターリンが1929年に彼の力を統一してから大部分は中止になった。1927年後半、カリーはプリンストン大学の講師として働いているときにそのコンビネータを再発見した。^[1]1930年代後半、アロンゾ・チャーチとプリンストン大学の彼の教え子が、combinatory logicよりも人気のあるラムダ計算という対抗するfunctional abstractionのための形式主義を考案した。理論計算機科学が60,70年代にcombinatory logicに関心を持ち始めるまで、これらの歴史的な偶発の結論は、ほとんどハスケル・カリーとその教え子、もしくはによるものだった。カリーとFeys、その他はcombinatory logicの初期の歴史について調査した。より近代的な並列処理のためのcombinatory logicとラムダ計算については、 Dana Scottが考案したcombinatory logicのためのモデル理論を60,70年代に批評したBarendregtを参照されたい。

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

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

combinatory logicはラムダ計算の変種としても見ることができる。ラムダ式(ラムダ抽象)は、束縛変数のない原始的な関数「コンビネータ」の有限集合によって置き換えられる。ラムダ式をコンビネータ式に変換するのは簡単であり、またコンビネータの簡約はラムダの簡約よりもシンプルである。Hence combinatory logicは非正格関数型言語や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や乗算演算子のように振る舞う項を識別することが可能である。(チャーチエンコーディングを参照) ラムダ計算は計算としてほかのもっともらしい計算のモデル(チューリングマシンを含む)と同等の力があることが分かっている。つまり、あらゆる計算を行える他のモデルはラムダ計算で表現でき、逆もそうである。チャーチ・チューリングのテーゼによれば、両方のモデルはあらゆる可能な計算を表現できる。すべての計算が、ラムダ抽象と適用を基本とした変数の置き換えのシンプルな概念で表現できることは、おそらく驚くべきことである。しかし、さらに目覚ましいのは、ラムダ抽象も必要がないことである。Combinatory logicはラムダ計算と同等のモデルだが、ラムダ抽象は存在しない。ラムダ計算での式の評価は非常に複雑である(置換の意味論は変数を捉えるのを避けるためのかなりの気配りと共に決めなければならない)。対照的に、Combinatory logicの式の評価は、置換という概念が存在しないためはるかに簡単である。

Combinatory calculi

ラムダ抽象が関数を作るための唯一の方法だから、combinatory calculusの中では何かがそれを置き換えねばならない。combinatory calculusは、ラムダ抽象の代わりに、原始的な関数の有限集合を提供する。

Combinatory terms

combinatory termは以下の形式のうち一つを持つ:

x
P
(E₁ E₂)

xは変数、Pは原始的関数、(E₁ E₂) は項の適用である。原始的関数はコンビネータ、もしくは、自由変数を含まないラムダ項である。

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

combinatory logicでの簡約

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

(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 and 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)

<!- The combinatory representation, (S (K (S I)) (S (K K) I)) is much longer than the representation as a lambda term, λx.λy.(y x). This is typical. In general, the T[ ] construction may expand a lambda term of length n to a combinatorial term of length Θ(3ⁿ) ^[要出典]. --> (S (K (S I)) (S (K K) I))という表現は、ラムダ項としての表現λx.λy.(y x)よりもはるかに長い。これは一般的なことである。普通、T[ ]はラムダ項をΘ(3ⁿ) ^[要出典]に展開する。

T[ ] 変換について

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₂を置き換えるのと同じである。だから

       (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の形の項において終了させなければならない。

Simplification of the transformation

η-簡約

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に加え、Schönfinkelの論文では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システムを参照)。Schönfinkelのもとの論文では、今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)
       = Ω

<!- but Ω does not have a normal form, so we have a contradiction. But if (S I I Z) does not have a normal form, the foregoing reduces as follows: --> しかし、Ωは正規形を持たないため、矛盾している。もし、(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 of ライスの定理 says that there is no complete nontrivial predicate. A predicate is a combinator that, when applied, returns either T or F. A predicate N is nontrivial if there are two arguments A and B such that NA=T and NB=F. A combinator N is complete if and only if NM has a normal form for every argument M. The analogue of Rice's theorem then says that every complete predicate is trivial. The proof of this theorem is rather simple.

Proof: By reductio ad absurdum. Suppose there is a complete non trivial predicate, say N.
Because N is supposed to be non trivial there are combinators A and B such that
(N A) = T and
(N B) = F.

Define NEGATION ≡ λx.(if (N x) then B else A) ≡ λx.((N x) B A)
Define ABSURDUM ≡ (Y NEGATION)

Fixed point theorem gives: ABSURDUM = (NEGATION ABSURDUM), for
ABSURDUM ≡ (Y NEGATION) = (NEGATION (Y NEGATION)) ≡ (NEGATION ABSURDUM).

Because N is supposed to be complete either:

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

Case 1: F = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N A) = T, a contradiction.
Case 2: T = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N B) = F, again a contradiction.

Hence (N ABSURDUM) is neither T nor F, which contradicts the presupposition that N would be a complete non trivial predicate. QED.

From this undecidability theorem it immediately follows that there is no complete predicate that can discriminate between terms that have a normal form and terms that do not have a normal form. It also follows that there is no complete predicate, say EQUAL, such that:
(EQUAL A B) = T if A = B and
(EQUAL A B) = F if A ≠ B.
If EQUAL would exist, then for all A, λx.(EQUAL x A) would have to be a complete non trivial predicate.

応用

関数型言語のコンパイル

関数型言語は、ラムダ計算のシンプルながら全般的な意味論に基づいている場合が多い。 David Turnerは、SASLを実装するために彼のコンビネータを利用した。

Kenneth E. Iversonは、APLの後続として、J (プログラミング言語)でカリーのコンビネータを基本としたプリミティブを使用し、Iversonが「暗黙のプログラミング」と呼んだものを可能にした。それは、変数を含まない式で、そのようなプログラムで作業するための強力なツールに沿って行うプログラミングである。APLのような言語では、ユーザー定義の演算子を用いたclumsier mannerで暗黙のプログラミングが可能であることが判明した。(Pure Functions in APL and J)

論理学

カリー＝ハワード同型対応は、論理とプログラミングの間のつながりを意味する。すべての直観論理における定理の証明は、型付きのラムダ項の簡約に対応する。さらに、定理は型シグネチャによって識別されうる。具体的には、型付きコンビネータ論理は証明論におけるヒルベルトシステムに対応する。コンビネータK、Sは以下の公理に対応する。

AK: A → (B → A),

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

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

MP: from A and A → B infer B.

The calculus consisting of AK, AS, and MP is complete for the implicational fragment of the intuitionistic logic, which can be seen as follows. Consider the set W of all deductively closed sets of formulas, ordered by inclusion. Then $\langle W,\subseteq \rangle$ is an intuitionistic Kripke frame, and we define a model $\Vdash$ in this frame by

X\Vdash A\iff A\in X.

This definition obeys the conditions on satisfaction of →: on one hand, if $X\Vdash A\to B$ , and $Y\in W$ is such that $Y\supseteq X$ and $Y\Vdash A$ , then $Y\Vdash B$ by modus ponens. On the other hand, if $X\not \Vdash A\to B$ , then $X,A\not \vdash B$ by the deduction theorem, thus the deductive closure of $X\cup \{A\}$ is an element $Y\in W$ such that $Y\supseteq X$ , $Y\Vdash A$ , and $Y\not \Vdash B$ .

Let A be any formula which is not provable in the calculus. Then A does not belong to the deductive closure X of the empty set, thus $X\not \Vdash A$ , and A is not intuitionistically valid.

脚注

^ 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.
--------, 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]