查看“︁组合子逻辑”︁的源代码

'''组合子逻辑'''是[[Moses Schönfinkel]]和[[哈斯凱爾·加里]]介入的一种符号系统，用来消除[[数理逻辑]]中对[[变量]]的需要。它最近在计算机科学中被用做计算的理论模型和设计函数式编程语言的基础。它所基于的'''组合子'''是只使用函数应用或早先定义的组合子来定义从它们的参数得出的结果的[[高阶函数]]。

== 数学中的组合子逻辑 ==

组合子逻辑意图作为简单的元逻辑，它能澄清在逻辑符号中的量化变量的意义，并真正的消除对它们的需要。消除量化变量的另一种方式是[[蒯因]]的谓词函子。尽管多数组合子逻辑系统超出了一阶逻辑的表达能力，蒯因的谓词函子的表达能力等价于一阶逻辑（[[#Quine 1960 1966|Quine [1960] 1966]]）。

组合子逻辑的最初发明者Schönfinkel，在1929年之后基本停止了发表著作。Curry在1927年<ref name="Seldin 2006">{{cite journal|last=Seldin|first=Jonathan|title=The Logic of Curry and Church}}</ref>晚期于[[哥廷根大学]]读博士的时候重新发现了组合子。在1930年代后期，[[邱奇]]和他的学生在普林斯顿发明了一个竞争的函数抽象的形式化，就是[[lambda演算]]，它比组合子逻辑更加流行。这些历史上的意外事件的结果是直到在1960年代和1970年代理论计算机科学开始感兴趣于组合子逻辑，关于这个主题的几乎所有工作都是[[哈斯凯尔·柯里]]和他的学生们，或比利时的Robert Feys做的。Curry和Feys (1958)和Curry等人（1972） 纵览了组合子逻辑的早期历史。组合子逻辑和lambda演算的更现代的平行处置参见Barendregt（1984），他还评论了[[达纳·斯科特]]在1960年代和1970年代为组合子逻辑设计的[[域理论|模型]]。

== 计算中的组合子逻辑 ==

在计算机科学中，组合子逻辑被用做[[可计算性理论]]中[[计算]]和[[证明论]]的简化模型。这个理论尽管简单，但捕获了计算本质的很多根本特征。

组合子逻辑可以被看作是[[lambda演算]]的变体，它把lambda表达式（用来允许函数抽象）替代为'''组合子'''的有限集合，它们是不包含[[自由变量]]的原始函数。很容易把lambda表达式变换成组合子表达式，并且因为组合子归约比lambda归约要简单，它已经被用做用软件中的某些[[非严格编程语言|非严格]]的[[函数式编程]]语言和硬件的[[图归约机]]的实现基础。

还可以用很多其他方式来看待它，很多早年的论文证明了各种组合子到各种逻辑公理的等价性[Hindley and Meredith, 1990]。

== lambda演算概要 ==
{{main|lambda演算}}

lambda演算关注的是叫做lambda-项的对象，它们是下列形式之一的符号串：

* v
* λv.E1
*(E1 E2)

这里的v是变量名字，它取自预定义变量名字的无限集合，而E1和E2是lambda-项。形如λv.E1的项叫做'''抽象'''。变量v叫做抽象的[[形式参数]]，而E1是抽象的“主体”。

项λv.E1表示一个函数，它应用于一个参数，绑定形式参数v到这个参数，接着计算E1的结果值---就是说，它返回E1，带有v的所有出现被参数所替代。

形如 (E1 E2)的项叫做'''应用'''。应用建模函数调用或执行：调用E1所代表的函数，带有E2作为它的[[参数]]，并计算结果。如果E1（有时叫做applicand）是一个抽象，则这个项可以被归约：参数E2可以被代换如E1的主体中E1的形式参数的位置上，而结果是一个新的lambda项，它等价于旧的。如果一个lambda项不包含形如 (λv.E1 E2)的子项，则它不能被归约，而被称为是[[Beta范式|范式]]。

表达式E[v := a]表示接受项E并把v的所有自由出现替代为a的结果。所以我们写

:(λv.E a) => E[v := a]

出于方便，我们用 (a b c d ... z)来简写 (...(((a b) c) d) ... z)。（就是说，应用是[[结合性|左结合的]]）。

归约的这个定义的动机是捕获所有数学函数的本质行为。例如，考虑计算数的平方的函数。我们写

:x的平方是x*x

（使用"*"来指示乘法）。这里的x是这个函数的[[形式参数]]。要计算一个特定参数的平方，比如3，我们把它插入到这个定义中形式参数的位置上：

:3的平方是3*3

要求值表达式3*3的结果，我们必须诉诸我们关于乘法和数3的知识。因为任何计算都简单的就是在适当基本参数上的适当函数的计算的复合，这个简单代换原理足够捕获计算的本质机制。此外，在lambda演算中，概念比如'''3'''和'''*'''，不需要任何额外定义基本运算符或常量就可以表示出来。有可能在lambda表达式中确定一些项，在做适合的解释的时候，它们的表现得如同数3和乘法运算符。

已知lambda演算在计算性上等价于关于计算的任何其他似乎为真的模型（包括[[图灵机]]）的能力；就是说，可以在任何这些模型中完成的计算都可以用lambda演算表达，反之亦然。根据[[邱奇-图灵论题]]，这些模型都可以表达任何可能的计算。

可能令人惊奇，只使用基于对项中变量的简单文字代换的函数抽象和应用的简单概念，lambda演算可以表达任何可想象出来的计算。但是更加不寻常的是甚至抽象都是不需要的。'''组合子逻辑'''就是等价于lambda演算的计算模型，它不需要抽象。

== 组合子演算 ==

因为在lambda演算中抽象是制造函数的唯一方式，在组合子演算中必须有某种东西替代它。不再使用抽象，组合子演算提供了有限的基本函数的集合，其他函数可以用它们来构建。

=== 组合子项 ===

组合子项是下列形式之一：
* v
* P
*(E1 E2)
这里的v是一个变量，P是基本函数之一，而E1和E2是组合子项。基本函数自身是'''组合子'''，或不包含[[自由变量]]的函数。

=== 组合子的例子 ===

组合子的最简单的例子是'''I'''，恒等组合子，定义为

:('''I''' x) = x

对于所有的项x。另一个简单的组合子是'''K'''，制造常量函数：('''K''' x)是对于任何参数都返回x的函数，所以我们定义

:(('''K''' x) y) = x

对于所有的项x和y。或者，服从同lambda演算中多重应用同样的约定，

:('''K''' x y) = x

第三个组合子是'''S'''，它是应用的一般化版本：

:('''S''' x y z) = (x z (y z))

'''S'''首先将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)对于任何x，('''S''' '''K''' '''K''')自身不等于'''I'''。我们称这种项是[[外延相等]]的。'''外延相等'''捕获了函数的等式的数学概念：两个函数是相等的，如果它们对于相同的参数总是生成相同的结果。相反的，项自身捕获了函数的内涵相等的概念：两个函数是相等的，当且仅当它们有相同的实现。有很多实现恒等函数的方式；('''S''' '''K''' '''K''')和'''I'''是其中的方式，('''S''' '''K''' '''S''')也是。我们将使用词'''等价'''来指示外延相等，保留'''等于'''给同一的组合子项。

更有趣的组合子是[[不动点组合子]]或'''Y'''组合子，它可以用来实现[[递归]]。

=== S-K基的完备性 ===

可能会令人惊奇，事实上'''S'''和'''K'''可以组合起来生成外延相等于任何lambda项的组合子，所以依据邱奇-图灵论题，等价于任何可计算的函数。证明是提出一个变换T[ ]，它转换一个任意的lambda项到等价的组合子。

T[ ]可定义如下：

# T[V] = > V
# T[(E1 E2)] = >(T[E1] T[E2])
# T[λx.E] = > ('''K''' T[E])（如果x在E中没有自由出现）
# T[λx.x] = > '''I'''
# T[λx.λy.E] = > T<nowiki>[</nowiki>λx.T<nowiki>[</nowiki>λy.E<nowiki>]]</nowiki>（如果x在E中自由出现）
# T[λx.(E1 E2)] =>（'''S''' T[λx.E1] T[λx.E2]）

==== 把lambda项转换成组合子项 ====

例如，我们可以转换λx.λy.(y x)为组合子：

:   T[λx.λy.(y x)]
: = T<nowiki>[</nowiki>λx.T<nowiki>[</nowiki>λy.(y x)<nowiki>]]</nowiki>（通过5）
: = T[λx.('''S''' T[λy.y] T[λy.x])]（通过6）
: = T[λx.('''S''' '''I'''       T[λy.x])]（通过4）
: = T[λx.('''S''' '''I'''       ('''K''' x))]（通过3）
: = ('''S''' T[λx.('''S''' '''I''')] T[λx.('''K''' x)])（通过6）
: = ('''S''' ('''K''' ('''S''' '''I'''))   T[λx.('''K''' x)])（通过3）
: = ('''S''' ('''K''' ('''S''' '''I'''))   ('''S''' T[λx.'''K'''] T[λx.x]))（通过6）
: = ('''S''' ('''K''' ('''S''' '''I'''))   ('''S''' ('''K''' '''K''')   T[λx.x]))（通过3）
: = ('''S''' ('''K''' ('''S''' '''I'''))   ('''S''' ('''K''' '''K''')   '''I'''))（通过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'''))比相应的lambda项λx.λy.(y x)要长很多，这是典型的。一般的，T[ ]构造可以把长度为n的lambda项展开为长度为[[大O表示法|Θ]]（3<sup>n</sup>）的组合子项。

==== T[ ]变换的解释 ====

T[ ]变换的目的是要消除抽象。两个特殊情况，规则3和4是平凡的：λx.x明显等价于'''I'''，而λx.E明显等价于（'''K''' E），如果x在E中不是自由出现的。

前两个规则也是简单的：变量转换为自身；通过简单的转换applicand和参数到组合子，把在组合子项中允许的应用转换为组合子。

有趣的是规则5和6。规则5简单的声称要转换一个复杂的抽象为组合子，我们必须首先把它的主体转换成组合子，接着消除这个抽象。规则6实际上消除这个抽象。

λx.(E1 E2)是一个函数，它接受一个参数比如a，并把它代换到lambda项 (E1 E2)中x的位置上，生成 (E1 E2)[x : = a]。但是代换a到 (E1 E2)中x的位置上同于代换它到E1和E2二者中，所以

:(E1 E2)[x := a] =(E1[x := a] E2[x := a])

:   (λx.(E1 E2) a) = ((λx.E1 a) (λx.E2 a))
: =('''S''' λx.E1 λx.E2 a)
: = (('''S''' λx.E1 λx.E2) a)

通过外延相等，

:λx.(E1 E2) =('''S''' λx.E1 λx.E2)

所以，要找到等价λx.(E1 E2)的组合子，找到等价于 ('''S''' λx.E1 λx.E2)的组合子就足够了，而

:('''S''' T[λx.E1] T[λx.E2])

显然合适。E1和E2每个都包含严格的比 (E1 E2)更少的应用，所以递归必定终止于根本没有应用的lambda项之上---要么是一个变量，要么是形如λx.E的项。

=== 变换的简化 ===

==== η-归约 ====

通过'''T'''[ ]变换生成的组合子可以做的更小，如果我们采用'''η-归约'''规则：

:T[λx.(E x)] = T[E]（如果x在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''')  （通过η-归约）

这个组合子等价于早先的更长的那个：

:   ('''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），所有组合子都可从它复合而外延等于任何lambda项。这种基的最简单的例子是{'''X'''}:

:'''X''' ≡ λx.((x'''S''')'''K''')

不难验证：
:'''X''' ('''X''' ('''X''' '''X''')) =<sup>ηβ</sup> '''K'''而
:'''X''' ('''X''' ('''X''' ('''X''' '''X''')))) =<sup>ηβ</sup> '''S'''.

因为{'''K''', '''S'''}是基，得出{'''X'''}也是基。

==== B和C组合子 ====

除了组合子'''S'''和'''K'''之外，[[Moses Schönfinkel|Schönfinkel]]的著作中包含了现在叫做'''B'''和'''C'''的两个组合子，带有如下归约：

:('''C''' a b c) =(a c b)
:('''B''' a b c) = (a (b c))

他还解释了如何只使用'''S'''和'''K'''来表达它们。

这些表达式在把谓词逻辑或lambda演算转换成组合子表达式的时候非常有用。它们也被[[Haskell Curry|Curry]]和更后来的[[David Turner]]所使用，他们的名字已经关联到了它们的应用上了。使用这些组合子，我们可以扩展变换规则为如下：

# T[V] = > V
# T[(E1 E2)] = >(T[E1] T[E2])
# T[λx.E] = > ('''K''' T[E])        （如果x在E中不是自由的）
# T[λx.x] = > '''I'''
# T[λx.λy.E] = > T<nowiki>[</nowiki>λx.T<nowiki>[</nowiki>λy.E<nowiki>]]</nowiki>（如果x在E中是自由的）
# T[λx.(E1 E2)] => ('''S''' T[λx.E1] T[λx.E2])（如果x在E1和E2二者中是自由的）
# T[λx.(E1 E2)] => ('''C''' T[λx.E1] E2)（如果x在E1中是自由的，但在E2中不是自由的）
# T[λx.(E1 E2)] => ('''B''' E1 T[λx.E2])（如果x在E2中是自由的，但在E1中不是自由的）

使用'''B'''和'''C'''组合子，λx.λy.(y x)的变换如下：

:   T[λx.λy.(y x)]
: = T<nowiki>[</nowiki>λx.T<nowiki>[</nowiki>λy.(y x)<nowiki>]</nowiki><nowiki>]</nowiki>
: = T[λx.('''C''' T[λy.y] x)]     （通过规则7）
: = T[λx.('''C''' '''I''' x)]
: = ('''C''' '''I''')                   （η-归约）
: = '''C'''<sub>*</sub>（传统规范记号：'''X'''<sub>*</sub> = '''X''' '''I'''）
: = '''I''''（传统规范记号：'''X'''' = '''C''' '''X'''）

('''C''' '''I''' x y)的确归约到 (y x):
:  ('''C''' '''I''' x y)
: =('''I''' y x)
: =(y x)

'''B'''和'''C'''的目的是'''S'''的有限版本。'''S'''接受一个值，并把在应用之前，把它代换入applicand和它的参数内，'''C'''只在applicand内进行代换，而'''B'''只在参数内进行代换。

这些组合子的现代名字源于[[哈斯凱爾·加里]]在1930年的博士论文（参见[[B,C,K,W系统]]）。在[[Moses Schönfinkel|Schönfinkel]]的最初著作中，把现在的S, K, I, B和C分别叫做S, C, I, Z和T。

===== CL<sub>K</sub>与CL<sub>I</sub>演算 =====
在本文描述的'''CL'''<sub>K</sub>和'''CL'''<sub>I</sub>演算必须做出区分。这种区别对应于在λ<sub>K</sub>和λ<sub>I</sub>演算之间的区别。不同于λ<sub>K</sub>演算，λ<sub>I</sub>演算限制抽象为：
:λv.E1这里的v在E1中有至少一次自由出现。
作为结论，组合子'''K'''不出现在λ<sub>I</sub>演算和'''CL'''<sub>I</sub>演算中。'''CL'''<sub>I</sub>的常量有：'''I''', '''B''', '''C'''和'''S'''，这形成了所有'''CL'''<sub>I</sub>项可以从它复合出来的基，'''B'''和'''C'''模拟'''K'''。所有λ<sub>I</sub>项可以转换成等价的'''CL'''<sub>I</sub>组合子，依据类似于前面提供的把λ<sub>K</sub>项转换成'''CL'''<sub>K</sub>组合子的规则。参见Barendregt (1984)第9章。

=== 逆转换 ===

从组合子项到lambda项的转换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[(E1 E2)] =（L[E1] L[E2]）

但是，要注意这个变换不是我们见到的任何版本的'''T'''[ ]的逆变换。

== 组合子演算的不可判定性 ==

一个组合子项是否有规范形式，两个组合子项是否是等价的等等都是不可判定的。者等价于
lambda项相应问题的不可判定性。但是，有一个直接证明如下：

首先，观察到项

: '''Ω''' = ('''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''',如果x有规范形式
:                '''F''',没有规范形式。

(这里的'''T'''和'''F'''是常规的lambda演算的真假定义λx.λy.x和λx.λy.y的变换。
组合子版本是'''T''' = '''K'''和'''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)   （'''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''')   （'''N'''的定义）
: = '''Ω'''

但是'''Ω'''没有规范形式，所以我们得到矛盾。但是如果 ('''S''' '''I''' '''I''' Z)没有规范形式，则前述归约为如下：

:   ('''N''' ('''S''' '''I''' '''I''' Z) '''Ω''' '''I''')
: = ('''K''' '''I''' '''Ω''' '''I''')   （'''N'''的定义）
: =('''I''' '''I''')
: = '''I'''

这意味着 ('''S''' '''I''' '''I''' Z)的范式简单的是'''I'''，这是另一个矛盾。所以，假设的范式组合子'''N'''不存在。

== 应用 ==

=== 函数式语言的编译 ===

[[函数式编程语言]]经常基于lambda演算的简单而普遍的语义。

David Turner使用它的组合子实现了[[SASL (编程语言)|SASL]]编程语言。

[[Kenneth E. Iverson]]在他的[[J语言|J编程语言]]中使用了基于Curry的组合子的原语（primitive），J语言是[[APL语言|APL]]语言的后继者。这使得Iverson达成了[[隐式编程]]，就是说，编程采用不包含变量的函数表达式，并一起使用与这种程序共同工作的强力工具。结果是在任何带有用户定义算子的类APL语言中隐式编程都是可能的<ref>{{cite journal |title=Pure Functions in APL and J |journal=Proceedings of the International Conference on APL '91 |first=Edward |last=Cherlin |pages=88–93 |year=1991 |doi=10.1145/114054.114065|isbn=0897914414 }}</ref>。

=== 逻辑 ===

[[Curry-Howard同构]]蕴涵了在逻辑和编程之间的联系：每个[[直觉逻辑]]的有效的定理证明都直接对应于一个有类型的lambda项的归约，反之亦然。定理自身也通过函数类型标志（signature）来识别。特别是，有类型的组合子逻辑对应于[[证明论]]中的[[希尔伯特系统]]。

'''K'''和'''S'''组合子对应于公理
:'''AK''': A → (B → A),
:'''AS''': (A → (B → C))  →  ((A → B) → (A → C)),
而函数应用对应于肯定前件规则
:'''MP''':从A且A → B推出B。

由'''AK''', '''AS'''和'''MP'''组成的演算对于直觉逻辑的蕴涵片段是完备的。考虑所有演绎闭合的公式的集合W，按[[子集|包含]]排序。则<math>\langle W,\subseteq\rangle</math>是直觉[[关系语义|Kripke框架]]，我们定义在这个框架内的模型<math>\langle W,\subseteq,\Vdash\rangle</math>为
:<math>X\Vdash A\iff A\in X.</math>
这个定义服从对→的满足的条件：在一方面，如果<math>X\Vdash A\to B</math>，并且<math>Y\in W</math>使得<math>Y\supseteq X</math>且<math>Y\Vdash A</math>，则通过肯定前件而<math>Y\Vdash B</math>。在另一方面，如<math>X\not\Vdash A\to B</math>，则通过[[演绎定理]]而<math>X,A\not\vdash B</math>，因此<math>X\cup\{A\}</math>的演绎闭包是<math>Y\in W</math>的一个元素使得<math>Y\supseteq X</math>, <math>Y\Vdash A</math>和<math>Y\not\Vdash B</math>。

设A是在演算中不能证明的任何公式。则A不属于非空集合的演绎闭包X，所以<math>X\not\Vdash A</math>，而A不是直觉有效的。

== 参见 ==
* [[SKI组合子演算]]
* [[B,C,K,W系统]]
* [[不动点组合子]]
* [[图归约机]]
* [[超组合子]]
*[[柯里化]]
*[[λ演算]]
*[[极小化求值]]
*[[求值策略]]

== 注釋 ==
{{reflist}}
== 引用 ==
* [[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 978-0-674-32449-7  The article that founded combinatory logic.
* {{cite book
| last = Curry
| first = Haskell B.
| coauthors = Robert Feys
| title = Combinatory Logic Vol. I
| volume = 1
| year = 1958
| publisher = North Holland
| location = Amsterdam
}}
* {{cite book
| last = Curry
| first = Haskell B.
| coauthors = J. Roger Hindley and Jonathan P. Seldin
| title = Combinatory Logic Vol. II
| volume = 2
| year = 1972
| publisher = North Holland
| location = Amsterdam
| id = ISBN 978-0-7204-2208-5
}}
* Field, Anthony J. and Peter G. Harrison, 1998. Functional Programming. . Addison-Wesley. ISBN 978-0-201-19249-0
* Paulson, Lawrence C., 1995. [http://www.cl.cam.ac.uk/Teaching/Lectures/founds-fp/Founds-FP.ps.gz Foundations of Functional Programming.] {{Wayback|url=http://www.cl.cam.ac.uk/Teaching/Lectures/founds-fp/Founds-FP.ps.gz |date=20170705155443 }} University of Cambridge.
* Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. [https://web.archive.org/web/20051016213140/http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf Lectures on the Curry-Howard Isomorphism.] University of Copenhagen and University of Warsaw, 1999.
* [https://web.archive.org/web/20040406093224/http://www.sadl.uleth.ca/gsdl/cgi-bin/library?a=p&p=about&c=curry 1920-1931 Curry'''s block notes]
* Hindley, Roger, and Meredith, 1990, "Principal Type-Schemes and Condensed Detachment," Journal of Symbolic Logic 55: 90-105
* [[Hendrik Pieter Barendregt]], 1984. The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, Volume 103, North-Holland. ISBN 978-0-444-87508-2
* <span id="Quine 1960 1966">[[Willard Van Orman Quine|Quine, W. V.]], [1960] 1966. "Variables explained away." Chapter 23 in W. V. Quine, Selected Logic Papers, 227–235. New York: Random House. Originally read by invitation to the American Philosophical Association in April 1960 and published in their Proceedings.</span>

{{CPU technologies}}
{{Authority control}}

[[Category:递归论]]
[[Category:计算模型]]
[[Category:组合子逻辑|*]]
[[Category:形式逻辑系统]]