组合逻辑 combinatory (Katalin Bimbó)
首次发表于 2008 年 11 月 14 日，实质修订于 2020 年 11 月 16 日。
组合逻辑（以下简称：CL）是一种优雅而强大的逻辑理论，与逻辑的许多领域有关，并在其他学科中找到应用，特别是在计算机科学和数学中。
CL 最初是作为经典一阶逻辑（FOL）中逻辑常量集合化简为单例集合的延续而发明的。CL 解决了替换问题，因为可以通过插入组合子为绑定变量的消除准备公式。从哲学角度来说，没有绑定变量的表达式代表了原始公式的逻辑形式。有时，绑定变量被认为是“本体论承诺”的标志。CL 的另一个哲学作用是展示一个理论的本体论假设的可变性。
替换不仅在一阶逻辑中是关键操作，而且在高阶逻辑以及包含变量绑定运算符的其他形式系统中也是如此，例如 λ 演算和 ε 演算。事实上，在 λ 演算和密切相关的函数式编程语言中，正确进行替换是特别紧迫的。尽管 CL 没有变量绑定运算符，但它可以模拟 λ 抽象。这使得 CL 成为函数式编程语言编译的合适目标语言。
与 λ-演算的联系可能会正确地暗示，CL 足够表达递归函数（即可计算函数）和算术。因此，CL 容易受到哥德尔类型的不完全性定理的影响。
CL 是一个典型的术语重写系统（TRS）。这些系统包括从编程语言的句法规范和无上下文文法到马尔可夫算法的各种形式的计算。甚至一些数论问题也可以看作是关于 TRS 的特殊实例的问题。一些最初为 CL 发明的概念和证明技术后来被证明在应用于不太理解的 TRS 时非常有用。
CL 通过类型与非经典逻辑相连接。首先，在直觉主义逻辑的蕴涵片段中可证明的公式与可类型化的组合术语之间发现了一种对应关系。然后，这种同构性被推广到其他组合基础和蕴涵逻辑（如相关蕴涵逻辑、无指数线性逻辑、仿射逻辑等）。
自我参照因素涉及一些悖论，例如广为人知的谬论悖论和罗素悖论。函数的集合论理解也不鼓励自我应用的想法。因此，纯无类型的组合逻辑并不排除函数的自我应用。此外，它的数学模型表明，函数可以成为自己的参数的理论是完全合理的，而且是一致的（这是早期使用证明论方法建立的）。
1. Schönfinkel 对绑定变量的消除
1.1 替换问题
古典一阶逻辑包括用 ∀（“对于所有”）和 ∃（“存在一个”）表示的量词。例如，“所有的鸟都是动物”可以形式化为 ∀x(Bx⊃Ax)，其中 x 是一个变量，B 和 A 是一元谓词，⊃ 是（物质）蕴涵的符号。在封闭公式 ∀x(Bx⊃Ax)中，变量的出现是被绑定的，而在开放公式 Bx⊃Ax 中，变量的出现是自由的。如果我们假设 t（代表“Tweety”）是一个名字常量，那么上述句子的一个实例是 Bt⊃At，可以理解为“如果 Tweety 是一只鸟，那么 Tweety 是一只动物。”这说明（普遍）量词的实例化涉及到替换。
由于示例的简单性，Bx 和 Ax 中 t 替换 x 似乎很容易理解和执行。然而，FOL（以及一般情况下，抽象语法，即带有变量绑定运算符的语言）的替换定义必须保证在结果表达式中，被替换表达式中的自由变量不会变为绑定变量。
为了看出可能出现的问题，让我们考虑（开放的）公式 ∀x(Rxy∧Rxr)，其中 R 是一个二元谓词，r 是一个缩写为“Russell”的常量名，∧ 是合取。∀x(Rxy∧Rxr)包含 y 的自由出现（即，y 是公式的自由变量），然而，y 对于包含自由出现的 x 的项的替换并不是自由的，例如，x 本身。更正式地说，在 ∀x(Rxy∧Rxr)中，R 的第二个参数位置中的 y 的出现没有被公式的量词（唯一的量词）绑定，而 ∀x(Rxx∧Rxr)是一个封闭的公式，即，它不包含自由变量的出现。非正式地说，以下自然语言句子可以被认为是对前面公式的解释。“每个人都读他和 Russell”（其中“他”是指示性的，或者也许是指代性的），以及“每个人都读自己和 Russell。”显然，这两个句子的意义大不相同，即使我们假设每个人都写了些东西。相比之下，∀x(Rxw∧Rxr)对于自由出现的 y 的名字常量 w 的替换是没有问题的。（后一个公式也许可以形式化为句子“每个人都读 Ludwig Wittgenstein 和 Russell。”）这些例子旨在演示摩西·舍恩菲克尔试图解决的问题的更复杂部分，以及他发明组合逻辑的原因。[1]
1.2 “nextand”和“U”运算符
关于经典命题逻辑（SL）的一个众所周知的结果是，所有真值函数都可以用 ¬ 和 ∧（或者 ¬ 和 ∨ 等）来表示。然而，一个最小充分的连接词集合可以只包含一个连接词，比如 ∣（通常称为 Sheffer 的竖线）或 ↓（Peirce 的联合否定）。“Nand”是“not-and”的意思，换句话说，A∣B 被定义为 ¬（A∧B），其中 A，B 是公式，¬ 是否定。反过来，如果 ∣ 是原始的，那么 ¬A 可以定义为 A∣A，A∧B 可以定义为（A∣B）∣（A∣B）。虽然带有许多竖线的公式可能很快变得视觉上混乱和难以解析，但很容易证明 ∣ 单独就足够表达所有的真值函数。
Schönfinkel 的目标是最小化需要用于 FOL 形式化的逻辑常量的数量，就像 Henry M. Sheffer（实际上，Charles S. Peirce）为经典命题逻辑所做的那样。上面提到的两个量词中的一个就足够了，而另一个可以假定已经被定义。我们可以说，∃xA 是 ¬∀x¬A 的缩写。即使将 ¬ 和其他连接词替换为 ∣，仍然会保留两个逻辑常量：∀ 和 ∣。另一个紧迫的问题是量词可以嵌套（即，一个量词的范围可能完全包含另一个量词的范围），并且变量绑定（可以通过在量词和它们绑定的变量之间画线来可视化）可能会变得非常复杂。暂时保留熟悉的逻辑常量，我们可以看一下下面的公式，它暗示了出现的困难——当考虑到问题的完全普遍性时。[2]
∀x（∃y（Py∧Bxy）⊃∃y（Py∧Bxy∧∀z（（Rz∧Ozy）⊃¬Cz）））
∀x 绑定 x 的所有出现；两个 B 的第二个参数位置的变量由两个 ∃ys 之一绑定，后者通过 Ozy 与 ∀z 交互。
在 FOL 中，谓词具有固定的有限元数，没有任何东西阻止一次绑定一个谓词的第一个参数和另一个谓词的第二个参数。（实际上，如果不通过某种补偿手段排除这种绑定，FOL 将失去一些表达能力。）当一个公式转化为前束范式中的一个（等价）公式时，这些困难仍然存在。只要变量绑定可以交织和编织成任意复杂的模式，似乎没有办法消除绑定变量。（请注意，开放公式中的自由变量在某种意义上表现得像局部名称常量，它们的消除既不是预期的，也不是在这里描述的过程中实现的。）
Schönfinkel 的巧妙之处在于他引入了组合子来解开变量绑定。组合子 S、K、I、B 和 C（以现代符号表示）是他的发明，并且他证明了 S 和 K 足以定义所有其他组合子。实际上，他还定义了一种算法来消除绑定变量，这本质上是现今用于在 CL 中定义括号抽象的算法之一。[3]
Schönfinkel 引入了一个新的逻辑常量 U，它表示两个类的不相交性。例如，当 P 和 Q 是一元谓词时，UPQ 可以用通常的 FOL 符号表示为 ¬∃x(Px∧Qx)。（该公式可以被认为是形式化了自然语言句子“没有鹦鹉是安静的。”）在消除约束变量的过程中，从包含“Xx”和“Yx”的表达式中获得 UXY，其中 x 不出现在 X 或 Y 中。例如，如果 X 和 Y 恰好是 n 元谓词，其中 n≥2，则 x 仅出现在它们的最后一个参数位置上。“没有人读亚里士多德和柏拉图”可以形式化为 ¬∃x(Rxa∧Rxp)，其中 a 和 p 是代表“亚里士多德”和“柏拉图”的名称常量。这个公式不能写成 U(Ra)(Rp)。另一方面，“没有人被罗素和维特根斯坦都读过”，即 ¬∃x(Rrx∧Rwx)转化为 U(Rr)(Rw)，其中括号标明了 U 的参数。通常，表达式 X 和 Y（在 UXY 中）由谓词（和名称常量）以及组合子和其他 U 组成。
有一个表示“下一个与”（即“不存在且”）的符号是有用的，而不假设 x 在连接的表达式中有自由出现，或者如果它有一个自由出现，则它是表达式的最后一个组成部分。继续使用 Schönfinkel 的方法，我们使用 ∣x 作为绑定 x 的“下一个与”运算符。（符号 ∣−，其中 − 是一个变量的位置，与 Sheffer 竖线非常相似。）Schönfinkel 实现了将 FOL 的逻辑常量集合减少到一个单例集合{∣−}的目标，因为 FOL 的每个公式都等价于只包含“下一个与”的公式。
通常情况下，即使 A 中没有 x 的自由出现，公式 ∀xA 在 FOL 中也被定义为良构的。那么，当然，∀xA 与 A 以及 ∃xA 等价，这样的量词被称为虚无的。为了证明任何公式都可以重写为只包含“nextand”的等价公式，只需检查以下关于 ¬、∨ 和 ∀（带有适当变量）的定义即可，这些定义归功于 Schönfinkel。
¬A⇔dfA∣xAA∨B⇔df(A∣yA)∣x(B∣yB)∀xAx⇔df(Ax∣yAx)∣x(Ax∣yAx)
例如，对于 ¬ 的定义可以通过以下等价关系来证明。A⇔A∧A，A∧A⇔∃x(A∧A)（假设 x 在 A 中不是自由的），因此通过替换，¬A⇔¬∃x(A∧A)。
现在我们给出一个具体的例子来说明如何将 FOL 的公式转化为只包含 ∣− 的公式，然后如何使用 U 和组合子来消除绑定变量。为了给这个过程增添一些激动人心的元素，我们从句子(#1)开始。
(#1)对于每个自然数，都存在一个更大的质数。
对于这个句子的一个直接形式化——在数字域的前景下——是公式(#2)，（其中'Nx'表示“x 是一个自然数”，'Px'表示“x 是一个质数”，'Gxy'的含义是“x 大于 y”）。
(#2)∀y∃x(Ny⊃(Px∧Gxy))
这个公式等价于 ∀y(Ny⊃∃x(Px∧Gxy))，进一步等价于 ¬∃y¬(Ny⊃∃x(Px∧Gxy))。在一两步之后，我们得到 Ny∣y(Px∣xGxy)。（除非括号另有说明，否则表达式被认为是向左分组的。例如，Gxy 是((Gx)y)，而不是根据 FOL 公式中最常见的括号排列方式可能预期的 G(xy)。）不幸的是，最后一个表达式中的 ∣x 和 ∣y 都不能被 U 替换。然而，如果 G 的参数被置换，那么前面的简化就可以进行。其中一个组合子 C 恰好可以满足要求：Gxy 可以改为 CGyx（请参见第 2.1 节中组合子的定义）。也就是说，我们有 Ny∣y(Px∣xCGyx)，然后得到 Ny∣yUP(CGy)。这个表达式可能会给人一种印象，即 y 是 UP(CGy)的最后一个组成部分，是 ∣y 的第二个参数，但事实并非如此。表达式内部的分组不能被忽视，还需要另一个组合子 B 将 UP(CGy)转换为所需的形式 B(UP)(CG)y。从 Ny∣yB(UP)(CG)y，我们在再进行一步得到 UN(B(UP)(CG))。这个表达式完全没有变量，并且它还使得 FOL 中的绑定变量重命名变得容易理解：给定两个（不同的）变量序列，它们在前两个元素上不同，上述过程的逆过程产生的公式是（逻辑等价的）字母变体，与(#2)中的公式相同。
表达式 UN(B(UP)(CG))与 FOL 公式的符号表示相比可能看起来“陌生”，但符号表示在很大程度上是一种约定。值得注意的是，第一个 U 后面只是跟着它的两个参数，然而第二个 U 不是这样。B(UP)是一个子表达式，但 UP(CG)不是 UN(B(UP)(CG))的子表达式。此外，整个表达式可以使用组合子转换为 XNPG，其中 X 仅由 U 和组合子组成。这样的 X 简洁地编码了带有谓词作为参数的公式的逻辑形式或逻辑内容。[5]
通过上述转换得到的表达式很快变得冗长，比如试图重写一个简单的 FOL 句子 ∃x(Px∧Qx)就可以看出。[6] 然而，这并不减弱 Schönfinkel 的理论结果的重要性。表达式长度的轻微增加（如果有的话）甚至不会带来任何不便，在拥有拍字节（甚至是艾克萨字节和泽塔字节）内存的计算机时代更是如此。
看起来令人遗憾的是，Schönfinkel 对 FOL 的简化过程并不广为人知。作为 Sheffer 和 Schönfinkel 简化过程知名程度的一个衡量标准，我们可以看到前者是逻辑学标准入门课程的一部分，而后者则不是。毫无疑问，其中一个原因是 Schönfinkel 的消除约束变量的过程在概念上更加丰富，而不是仅仅从 ∣（或 ↓）定义几个真值函数。另一个原因可能是 Schönfinkel 可能没有足够强调通过“nextand”来消除所有其他逻辑连接词和量词的中间步骤。这一步骤的重要性在 Schönfinkel 的论文英文译本的引言中也被忽视了，该译本是在原始出版物发表 30 多年后撰写的。我们还可以注意到，虽然“nextand”在标准逻辑意义上是一个运算符，但它是二元的，不像 ∀ 和 ∃ 那样是一元的。
如果将 A∣B⇔df¬(A∧B)添加为 SL 的定义，则结果是一种保守扩展，并且可以证明对于任何公式 A(p0,…,pn)（即包含显示的命题变量和一些连接词的公式），存在一个只包含连接词 ∣ 的公式 B(p0,…,pn)，且 B(p0,…,pn)⇔A(p0,…,pn)本身是可证的。当然，“nand”作为二元连接词或二元真值函数与合取、析取等对象属于同一类别。
Schönfinkel 对 FOL 的扩展的第一阶段是类似的。添加 ∣− 也是 FOL 的保守扩展，可以消除每个 ∣− 的出现。（我们注意到 ∣− 是一个二元运算符，因此可以认为它将量词（∃）与连接词（¬、∧）结合在一起，但 ∣− 当然不会引入在 FOL 中无法定义的任何对象。）
Schönfinkel 对 FOL 的扩展的第二阶段略有不同。只有对于一元谓词 P 和 Q（或者对于最后一个参数中的变量绑定的高阶谓词），UXY 才能在 FOL 中定义。因此，一般情况下，U 和组合子都不能在 FOL 中定义。
绑定变量的消除超出了 FOL 的资源。组合子不仅无法定义，而且它们是一种新的对象，这些对象在 FOL 本身中是不存在的。此外，绑定变量消除过程的中间步骤假设多个参数的函数可以被视为一个变量的函数，反之亦然。[7] 在 FOL 的表达中引入具有足够多正确顺序的谓词符号将是比较无问题的，并且它将为语言添加与其他谓词具有相同解释方式的对象。然而，一个潜在的问题是，对于每个谓词，都需要无限多（ℵ0 多）个新谓词，以及规定谓词变体之间意义的等价性的公理。在符号上，这些步骤相当于用额外的参数填充谓词符号，省略一些参数，以及对参数进行排列和重新分组。尽管其中一些添加可能看起来是多余的或过于繁琐，但对于理解 Schönfinkel 的消除绑定变量的过程来说，关键是要注意公式被视为结构化的符号字符串。[8]
总结这一部分时，强调重要的是，关于上述简化过程的一致性问题是不存在的，因为它可以被视为一个明确定义的算法，或者用当代术语来描述。然而，如果我们考虑到用组合子扩展的 FOL 语言，那么得到的系统是不一致的，因为 CL 足够强大，可以定义任何函数的不动点。拥有所有函数的不动点（包括真值函数）的效果可以被认为是添加了某些双条件（可能有效，也可能无效）作为公理。（例如，罗素悖论源于否定连接词的不动点。）值得注意的是，FOL 和（纯粹的）CL 都是一致的。
1.3 替代方法：基本逻辑和谓词函数
在本节中，我们简要概述了两个与 Schönfinkel 的工作相关或受到他在消除约束变量中使用组合子的启发的思想。
菲奇的金属逻辑* 从 20 世纪 30 年代末开始，弗雷德里克·菲奇致力于研究一种他称之为基本逻辑的逻辑学。这个标签的动机是他的目标是提供一个框架，可以在其中形式化任何逻辑。菲奇的方法完全是句法的（类似于舍恩芬克尔的方法），而“形式化”是指将一个形式上描述的系统编码成另一个系统，这与哥德尔的不完全性定理中的语法算术化类似。
1942 年，菲奇引入了一个他标记为 K 的逻辑。K 中的表达式类似于组合术语，通过一个二元应用操作形成，该操作不被假定为可结合的。（请参见下一节中对组合术语的定义。）然而，K 的常量与纯 CL 的常量不重合。菲奇使用了 10 个常量：ε，o，´ε，´o，W，=，∧，∨，E 和 ∗。前五个常量是组合子，尽管符号可能暗示了不同的（非正式）含义。‘=’是表达式的语法标识。‘∧’和‘∨’意味着“与”和“或”。‘E’是舍恩芬克尔的 U 的类比，但它对应于一个非空的存在量词。最后，‘∗’类似于二元关系的传递闭包运算符或克林星号。值得注意的是，该系统中没有否定或全称量词。常量的使用如下所述，有点类似于公理表征组合子。
=ab 当且仅当 a 和 b 是（语法上）相同的表达式
εab 当且仅当 ba
oabc 当且仅当 a(bc)
´εabc 当且仅当 bac
´oabcd 当且仅当 a(bc)d
Wab 当且仅当 abb
∧ab 如果且仅当 a 和 b
∨ab 如果且仅当 a 或 b
Eb 如果且仅当 存在 a. ba
∗abc 当且仅当 abc 且 ∃d.abd&adc
在 CL 中，公理后面跟着诸如一步和弱约简的概念，后者可以看作是计算或推理步骤。（有关这些概念的一些内容，请参见下一节。）类似地，对于 FOL 的公理演算，除了公理外还包含推理规则。穿透基本逻辑的各种表达方式的障碍之一是缺乏类似的表述。
在他第一篇关于基本逻辑的论文发表后的接下来的二十年左右，Fitch 发表了一系列关于基本逻辑的论文，主要涉及以下内容：（1）递归函数的表示（即语法的算术化的可能性的证明），（2）K'，K 的扩展，包括否定、全称量词和#（∗ 运算符的对偶），（3）K 和 K'的一致性，（4）L，K'的扩展，包括蕴涵和必然性运算符，（5）一些常量的可定义性，如 ∗ 和#，以及 E。
包含在 K 中（因此也包含在其所有扩展中）的组合子有 T、B 和 W。´ε 和 ´o 分别是 T 的三元版本和 B 的四元版本。罗素悖论涉及否定，但（Curry 悖论的任何变体）都是积极的，因为它依赖于 David Hilbert 的积极蕴涵逻辑的一个或两个定理。这意味着，如果各种基本逻辑系统，特别是 K'和 L 是一致的，那么它们要么不能包含完全抽象，要么蕴涵、推演和身份的概念应与它们通常的对应物不同。实际上，K、K'和 L 都不是外延系统。也就是说，即使两个应用于相同表达式的表达式总是相等的，应用表达式的相等性也不成立。将基本逻辑转化为外延系统的过程证明并不简单。Fitch 的 JE'系统被 Myhill 证明是不一致的，这导致了对外延身份条件更复杂的制定。
基本逻辑尚未成为广泛使用的形式系统描述的通用框架；然而，对这种方法的重新关注可以从 Updike（2010）中看出，该文试图将基本逻辑置于 20 世纪中叶基础性工作的更广泛背景中。
奎恩的消除策略 从 1930 年代末开始，W.V.O.奎恩致力于一种替代方法，以消除一阶逻辑中的约束变量。可以合理地假设，舍恩芬克尔的目标是在经典逻辑中找到一个单一的运算符，然后消除约束变量 - 正如他在舍恩芬克尔（1924）中所声称的那样 - 而不是定义一个总体的符号系统来描述所有数学。然而，CL 很快以一种更自由的方式与经典逻辑融合在一起，导致了一个不一致的系统。
奎恩通过对某种程度上类似于组合子的常量进行隐式类型化，找到了避免不一致性的方法。他将这些常量称为谓词函子，并引入了几组谓词函子，其中最后一组出现在奎恩（1981）中。
FOL 的最常见表述规定，一个 n 元谓词后跟一系列 n 个项（可能由逗号分隔并用括号括起来）是一个公式。（这与舍恩芬克尔对公式的观点相反，并符合谓词作为 n 元关系的非正式和形式解释。换句话说，FOL 不允许谓词或其解释的“柯里化”。）奎恩认同项序列跟随谓词的观点。
谓词函数符不适用于彼此，不像组合子那样。这是奎因反复强调的一点。原子谓词是一阶语言的谓词，而复合谓词是通过将谓词函数符（适当的元数）应用于谓词（可以是原子的或复合的）而获得的。
禁止自我应用以及使用“平坦”的参数序列意味着需要无限多个谓词函数符来确保从 FOL 的所有公式中消除约束变量。为了快速解释问题：否则无法确保任意远距离的一对元素的排列。正如组合子可以根据其效果分为不同的组，奎因能够选择可以根据其效果自然分组的谓词函数符。实际上，谓词函数符的组类似于组合子的类，尽管奎因的标签常常崇高。为了给出这种替代方法的具体示例，我们概述了奎因（1981）的一组稍微修改过的谓词函数符。
假设只有 ∣− 作为唯一运算符的一阶语言。（F 和 G 是谓词函数语言中的谓词的元变量。）对于每个 n∈ω，≀n Invn，invn，Padn+1 和 Refn 都是谓词函数符。通过应用以下子句，将 FOL 的公式重写为谓词函数语言中的公式。
FOL 中的变量 x 和谓词 P 分别在谓词函子语言中表示为 x 和 P。
Fx1x2…xn∣x1Gx1x2…xn:=:(F≀G)x2…xn，其中 x2,…,xn 与 x1 不同，并且 F 和 G 后面跟着相同的变量序列。
Fx1x2…xn:=:(Inv F)x2…xnx1
Fx1x2…xn:=:(inv F)x2x1…xn
Fx2…xn:=:(Pad F)x1x2…xn
Fx1x1x2…xn:=:(Ref F)x1x2…xn
在 Ref 和 W，Pad 和 K，以及 Inv 和 inv 以及具有排列效应的各种组合子之间存在明显的相似性（例如 C 和 T）。如果 ∣− 是一阶语言中唯一的运算符，则所有不是原子的公式几乎都是形式为 2 中左侧表达式的形式。必须确保满足侧条件，这就是 3-6 条款的作用。尽管可以通过忽略未受影响的参数来混淆 ≀，inv，Pad 和 Ref 的各种 n-ary 版本，但 Inv 显然代表无限多个谓词函子，因为不能忽略或省略 x1,…,xn。
值得注意的是 ≀ 和 Schönfinkel 的 U 之间存在差异。不仅绑定变量的位置不同，而且 ≀ 为 n−1 个变量（由左侧表达式中的 ∣− 和其他符号分隔）构建了收缩。
Quine 打算使用谓词函子语言来引导一阶逻辑的新代数化。虽然可以使用谓词函子消除绑定变量，但 Quine 从未以通常意义上的代数定义过一种代数，类似于圆柱代数。谓词函子的设计具有非常有限的适用性，这不幸地导致它们似乎在其预期的上下文之外没有太大的兴趣和用途。
2. 组合术语及其主要属性
2.1 简化、等式及其形式化
格奥尔格·康托尔（Georg Cantor）和伯特兰·罗素（Bertrand Russell）在 19 世纪末 20 世纪初发现的悖论都涉及集合的自我成员关系。阿尔弗雷德·N·怀特海德（Alfred N. Whitehead）和伯特兰·罗素以及 ZF（以恩斯特·策梅洛（Ernst Zermelo）和亚伯拉罕·A·弗兰克尔（Abraham A. Fraenkel）命名的集合论形式化）的分层类型理论排除了自我成员关系。然而，似乎一直存在着一种希望创建一个允许自我成员关系或自我应用的理论的愿望。事实上，柯里（Curry）发展组合逻辑的动机之一就是构建一个包括各种良构表达式的形式语言，其中一些在特定解释下可能被证明是无意义的。（这个想法可以与冯·诺伊曼-伯纳斯-哥德尔集合论形式化相比较，在该形式化中，没有基础公理，罗素类可以被证明不是一个集合，因此是一个真类。）
为了阐明(1)这是一个良构（但无意义）的表达式和(2)这是一个有意义（但不良构）的句子之间的区别，以下是一些自然语言的例子。当然，(2)的意义应该带有一定的保留态度。实际上，库尔特·哥德尔在 1930 年证明了 PM 系统是不完备的。因此，(2)可能被猜测为(2′)哥德尔在 1930 年证明了皮亚诺算术是不完备的，这是通过句法和语义线索推断出来的扭曲版本。
(1)对于 λx(x2+4x−6)的导数希望宣称函数是聪明的。
(2)哥德尔在 1930 年证明了皮亚诺算术是不完备的。
在这些非正式的动机之后，我们转向逻辑学的适当部分，并更正式地介绍一些概念。
逻辑学中的对象称为术语。[9] 术语可以被认为是函数的解释（在第 4.1 节中进一步解释）。原始术语包括变量和常量，而复合术语是通过组合术语形成的。通常，包括可数集合（即具有基数 ℵ0 的集合）的变量，并且常量包括一些（未定义的）组合子。（我们在对象语言中使用 x、y、z、v、w、u、x0 等作为变量，而在范变量中使用 M、N、P、Q 等作为范围限定术语。）
术语的归纳定义如下。
(t1)如果 x 是一个变量，那么 x 是一个术语；
(t2)如果 c 是一个常量，那么 c 是一个术语；
(t3)如果 M 和 N 是术语，那么(MN)是一个术语。
在上述定义中，(t3)隐藏了将两个术语 M 和 N 连接的二元操作。这个操作被称为应用，通常用并置表示，即将其两个参数放在一起，如(MN)。
应用不被假设具有额外的属性（如可交换性），因为它的预期解释是函数应用。例如，((vw)u)和(v(wu))是不同的术语——就像对于 λx.x2+4x−6 的导数应用于 8（即(λx.2x+4)8=20）与对于 90 的导数（即(82+32−6)′=0）是不同的。使用 λ 符号，示例中的两个术语可以表示为
((λy.y′)(λx.x2+4x−6))8
对抗
(λy.y′)((λx.x2+4x−6)8).
如果将术语视为结构化字符串（其中括号表示分组），那么与长度为 n 的字符串相关联的不同术语的数量是卡塔兰数 Cn−1。对于非负整数 n（即 n∈N），
Cn=1n+1(2nn).
前七个卡塔兰数是 C0=1，C1=1，C2=2，C3=5，C4=14，C5=42 和 C6=132。为了简单起见，我们可以取由 xs 组成的字符串，因为这些项只在它们的组合方式上有所不同。显然，如果项是 x 或 xx，即长度为 1 或 2，则只有一种形成项的方式，即每种情况下只存在一个可能的项。如果我们从三个 xs 开始，那么我们可以形成(xx)x 或 x(xx)。如果项的长度为 4，则有五个项：xxxx，x(xx)x，xx(xx)，x(xxx)和 x(x(xx))。（尝试列出由 5 个 xs 可以形成的 14 个不同项是一个有用的练习。）
在 CL 中，通常的符号约定是将左关联的项与最外层的括号一起省略。例如，xyz 的完整写法是((xy)z)，而 xy(xz)和(xy)(xz)都是该项((xy)(xz))的“简写版本”（与 xyxz 不同）。项中的分组界定了子项。例如，xy 是本段提到的每个项的子项，而 yz 和 yx 都不是这些项的子项。
一个术语的子术语被递归地定义如下。
(s1)M 是 M 的子术语；
(s2)如果 M 是 N 或 P 的子术语，则 M 是 NP 的子术语。
顺便提一下，自由变量的概念现在可以直接定义了：如果 x 是 M 的子项，则 x 是 M 的自由变量。M 的自由变量集合有时用 fv(M)表示。
所有术语都被解释为函数，组合子也是函数。类似地，对于一些可以轻松描述和理解的数值和几何函数，经常遇到的组合子可以被描述为对术语的明显转换。（无衬线字母表示组合子，>表示一步规约。）
定义。（一些众所周知的组合子公理）
| Sxyz▹1xz(yz) | Kxy▹1x | Ix▹1x |
|---|---|---|
Bxyz▹1x(yz) | Txy▹1yx | Cxyz▹1xzy |
Wxy▹1xyy | Mx▹1xx | Yx▹1x(Yx) |
Jxyzv▹1xy(xvz) | B′xyz▹1y(xz) | Vxyz▹1zxy |
这些公理默示了组合子的元数以及它们的规约（或收缩）模式。也许，最简单的组合子是恒等组合子 I，它应用于参数 x 时返回相同的 x。K 应用于 x 时是一个常数函数，因为当它进一步应用于 y 时，它产生 x 作为结果，也就是说，K 是相对于其第二个参数的取消器。W 和 M 是复制器，因为在它们的应用结果中，一个参数（总是）出现两次。C、T 和 V 是置换器，因为它们改变了一些参数的顺序。B 是一个关联器，因为 Bxyz 变成了一个在 x 应用于结果之前 y 应用于 z 的术语。Y 是不动点组合子，因为对于任何函数 x，Yx 是该函数的不动点（见第 2.3 节）。组合子 B'是一个关联器和置换器，而 S 和 J 也是复制器。S 非常特殊，它被称为强合成组合子，因为当应用于两个函数，比如 g 和 f（按照这个顺序），以及 x 时，结果术语 gx(fx)表示 g 和 f 对同一个参数 x 的合成。
这些非正式的解释没有提及函数 x、y、z、f、g 等可能的限制。然而，上述公理限制了组合子对变量的适用性。直观上，我们希望说给定任何术语，也就是任何函数 M 和 N，WMN 可以一步规约为 MNN（可能作为另一个术语的子术语）。例如，M 可以是 K，N 可以是 yy，然后 WK(yy)▹1K(yy)(yy)。后一个术语暗示了进一步的一步规约，事实上我们可能对连续的一步规约感兴趣——比如从 WK(yy)到 yy 的规约。实现这些目标的一种方法是从标准的不等式逻辑开始形式化（一个理论的）CL，但省略反对称规则并添加某些其他公理和规则。
对于 CL（CL▹）的不等式演算。
| M▹M | SMNP▹MP(NP) | KMN▹M |
|---|---|---|
M▹NN▹PM▹P | M▹NMP▹NP | M▹NPM▹PN |
使用元变量包括替换（我们在上面对 WMN 术语进行了说明）。恒等公理和传递性规则意味着 ▹ 是一个传递且自反的关系。最后两个规则将应用特征化为在其两个参数位置上都是单调的操作。CL▹ 仅包括 S 和 K，因为其他组合子可以从它们中定义出来-正如我们在 1.2 节中已经提到的，并且正如我们在本节末尾更详细地解释的那样。
组合子集合{S，K}被称为组合基础，也就是说，这两个组合子是 CL▹ 的未定义常量。为了给出这个演算中的一个证明的思路，可以将以下步骤组合在一起证明 SKK(KSK)▹S。KSK▹S 是一个公理的实例。然后通过右单调性得到 SKK(KSK)▹SKKS，进一步，通过 S 和 K 公理的实例以及传递性规则的应用得到 SKK(KSK)▹S 的结果。
关系 ▹ 被称为弱规约，也可以用以下方式进行定义。（“弱规约”是 CL 中使用的技术术语，用于区分该术语在术语集合上的其他关系之一，其中之一被称为“强规约”。）一个形式为 SMNP 或形式为 KMN 的术语是一个约简，而前导组合子（分别为 S 和 K）是约简的头部。如果术语 Q 包含形式为 SMNP 的子术语，则通过将该子术语替换为 MP（NP）而获得的 Q′是 Q 的一步约简。（对于约简 KMN 和 M 也是如此。）也就是说，在这两种情况下，Q▹Q′。然后，规约可以被定义为一步规约的自反传递闭包。这个概念完全被 CL▹ 所捕捉。演算 CL▹ 在以下意义上是完备的，即如果 M▹N 在我们刚刚描述的意义上，那么 CL▹ 证明 M▹N。（很容易看出逆向蕴含也是正确的。）
规约的概念是比一步规约更弱的关系，因此使用更强的关系来区分术语的一个子类是有用的。当术语不包含约简时，它是正常形式（nf）中的一个术语。请注意，一步规约不需要减少术语包含的约简的总数，因此，并不是每个术语都可以通过有限次的一步规约转化为 nf 中的术语。实际上，有些术语不能约简为 nf 中的术语。
缩减可以说是表示函数之间重要关系的术语之间的关系。程序执行和其他具体计算中的典型步骤是函数应用，而不是另一个方向的移动，即所谓的扩展。然而，函数的相等概念在数学中是众所周知的，并且类似的概念也在 CL 中引入了。一步缩减关系的传递性、自反性、对称闭包称为（弱）相等。通过使用组合公理和规则扩展标准等式逻辑来形式化等式 CL。
CL（CL=）的等式演算。
| M=M | KMN=M | SMNP=MP(NP) | |
|---|---|---|---|
M=NN=PM=P | M=NN=M | M=NMP=NP | M=NPM=PN |
第一个公理和前两个规则构成了等式逻辑。常量再次是组合子 S 和 K。请注意，CL=也可以被定义为 CL▹ 的扩展，通过添加对称规则，这将与从缩减定义等式的传递性、对称闭包的描述相平行。相反，我们选择使用新的符号重复不等式公理和规则（并添加对称规则），使得这两个定义是自包含且易于理解的。=的这两种表征是相同的-就像 ▹ 的表征一样。
CL▹ 和 CL=共享一个可能是可取的特征，这取决于对函数理解的何种捕捉方式。为了说明这个问题，让我们考虑一元组合子 SKK 和 SK(KK)。很容易验证 SKKM▹M 和 SK(KK)M▹M。然而，在 CL▹ 中既不能证明 SKK▹SK(KK)，也不能证明 SK(KK)▹SKK；更不用说在 CL=中证明这两个术语的相等性了。这意味着 CL▹ 和 CL=形式化了函数的内涵概念，其中“内涵性”意味着在相同输入上产生相同输出的函数可能仍然是可区分的。
我们可能会遇到的典型内涵函数是算法。例如，我们可以考虑各种计算 π 的十进制展开的规范，或者行为相同的各种计算机程序。例如，编译器（对于同一种语言）可能因为使用或不使用某些优化而彼此不同，从而从给定的代码生成具有相同输入输出行为但运行时间不同的程序。
如果要识别在输入输出行为上无法区分的函数，也就是寻求函数的外延理解，那么 CL▹ 和 CL=必须通过以下规则进行扩展（其中符号‡分别替换为 ▹ 或=）。
Mx‡NxM‡N 其中 x 在 MN 中不是自由的。
2.2 Church–Rosser 定理和一致性定理
前一节的演算 CL▹ 和 CL= 形式化了约简和相等性。然而，▹ 和 = 在术语被认为代表函数时具有一些重要的附加属性。下一个定理是关于 CL 的最早和最著名的结果之一。
Church–Rosser 定理（I）。如果 M 归约为 N 和 P，则存在一个术语 Q，N 和 P 都可以归约为它。
图 1. Church–Rosser 定理（I）的示意图
如果我们认为归约类似于计算函数的值，那么 Church–Rosser 定理——在第一近似中——可以被认为是陈述了使用一个术语进行一系列计算的最终结果是唯一的，与步骤的顺序无关。然而，这是一个轻微的夸张，因为唯一性意味着每个计算序列都会结束（或者在一个术语上“循环”）。也就是说，如果存在唯一的最终术语，那么只有有限多个不同的连续计算步骤是可能的。
用初等算术运算进行粗略类比或许可以对情况有所启示。自然数的加法和乘法总是得到一个自然数。然而，如果包括除法，那么并不总是所有数值表达式都能求值为一个自然数，因为 7/5 是一个有理数而不是自然数，而 n/0 是未定义的（即使 n 是实数）。也就是说，有些数值表达式并不求值为（自然）数。虽然与组合术语的类比并不是非常紧密，但它是有用的。例如，假设函数 λn.n/0 的值域扩展以允许 r 是有理数，那么 n/0 可以通过计算机上的循环（如果 n≠0，则执行时永远不会终止）来实现，该循环将遍历有理数的枚举，试图找到一个 r，使得 r⋅0=n。
组合术语 WWW 和 WI(WI)或许是没有正规形式的最简单的例子。这两个术语都引发了一个无限的规约序列，即连续的一步规约的无限链。为了使例子更加透明，让我们暂时假设 W、I、C 等不是由 K 和 S 定义的，而是原始常量。在 WWW 中唯一的可约项的收缩返回相同的术语，这表明唯一性并不意味着该术语是正规形式。在 WI(WI)中唯一的可约项的收缩得到 I(WI)(WI)，进一步规约到我们开始的术语。一个稍微复杂一点的例子是 Y(CKI)，它只有无限规约序列。这个术语有一个规约序列（其中每个收缩的可约项以 Y 为首），其中包含无限多个不同的术语。还可以创建以 Y(CKI)开头并具有各种循环的无限规约序列。总之，通常情况下，Church-Rosser 定理不能保证术语 Q 的唯一性。然而，如果 M 有一个正规形式，那么它是唯一的。
教堂-罗瑟定理通常被陈述如下。
教堂-罗瑟定理（II）。如果 N 和 P 相等，则存在一个术语 Q，使得 N 和 P 都可以归约为 Q。
图 2. 教堂-罗瑟定理（II）的示意图
Church-Rosser 定理的第二种形式与第一种形式在其假设上有所不同。从将等式定义为规约的超集的角度来看，第一种形式的定理显然被第二种形式所蕴含。然而，尽管第二种形式的 Church-Rosser 定理的假设较弱，但这两个定理是等价的。等式是规约的传递性、对称闭包，这意味着如果两个术语相等，则存在一个由规约和扩展步骤组成的有限路径（分别分解为一步规约和一步扩展）。然后通过对连接 N 和 P 的路径长度进行有限次应用第一种 Church-Rosser 定理（即对路径长度进行归纳），第一种 Church-Rosser 定理蕴含了第二种形式。
对于 CL 的 Church-Rosser 定理的现代证明是间接进行的，因为一步规约不具备菱形性质。当二元关系 R（例如规约）满足 xRy 和 xRz 蕴含 yRv 和 zRv（其中 v 为某个项）时，称关系 R 具有菱形性质。如果二元关系 R 具有菱形性质，则其传递闭包也具有菱形性质。为了利用这一洞察力证明 Church-Rosser 定理，需要找到规约的适当子关系。所寻找的子关系应具有菱形性质，并且其自反传递闭包应与规约相一致。
以下反例说明了一个术语的一步规约可能导致进一步的术语不能在一步中规约到一个共同的术语。SKK(KKS)▹1SKKK 和 SKK(KKS)▹1K(KKS)(K(KKS))，然后可能的规约序列如下。
SKKK▹1KK(KK)▹1K
K(KKS)(K(KKS))▹1KKS▹1K
K(KKS)(K(KKS))▹1KK(K(KKS))▹1KK(KK)▹1K
K(KKS)(K(KKS))▹1K(KKS)(KK)▹1KKS▹1K
K(KKS)(K(KKS))▹1K(KKS)(KK)▹1KK(KK)▹1K
钻石属性的失败一旦我们注意到 SKKK▹1KK(KK) (仅仅), 但是 K(KKS)(K(KKS))不能在一步中减少到 KK(KK)。
适当的还原的子关系是一组不重叠的红式同时还原，用 ▹sr 表示。'不重叠'意味着两个红式之间没有共享的子项出现。▹sr 包括 ▹1，因为红式的一步还原可以视为红式的单例集合的 ▹sr。▹sr 显然包含在 ▹（即还原）中。这两个事实意味着 ▹sr 的自反传递闭包是还原——当考虑到自反传递闭包操作（用 ∗ 表示）的调性时。
（1）-（3）总结了所提及关系之间的关键包含关系。
（1）▹1⊆▹sr⇒▹∗1⊆▹∗sr
(2)▹sr⊆▹⇒▹∗sr⊆▹∗
(3)▹∗1⊆▹∗ and ▹∗=▹.
我们需要的 ▹sr 的核心属性是以下定理的内容。
定理。（▹sr 的钻石特性）如果 M▹srN 且 M▹srP，则存在一个术语 Q，使得 N▹srQ 且 P▹srQ。
该定理的证明是对术语 M 的简单归纳。▹sr 的属性保证可以同时执行一个或多个一步规约，但规约不能相互干扰（或重叠）。
CL 的一致性来自于 Church-Rosser 定理以及（至少两个）不同的正常形式的存在。
定理。（一致性）CL 是一致的，也就是说，存在一些术语彼此不归约，因此它们不相等。
并非所有术语都有一个正规形式，然而，许多术语确实有。首先，包括 S 和 K 在内的一些例子。（如果包括变量，其中有 ℵ0 个，它们都在正规形式中。）这些术语中没有一个包含一个 redex，因此每个术语只归约到自身。根据 Church-Rosser 定理，排除了某个术语 M 可以同时归约到 x 和 S（使 S 等于 x）的可能性。
无限归约序列和正规形式之间的相互作用值得更仔细地检查。术语 WWW，Y(CKI)和 WI(WI)只有无限归约序列。然而，一个术语存在无限归约序列并不意味着该术语没有正规形式（当组合基是完备的或包含一个取消器时）。Y(KI)归约到 KI(Y(KI))，KI(KI(Y(KI)))，KI(KI(KI(Y(KI))))，…以及 I。
一个术语在具有 nf 时弱规范化，而当其所有的规约序列都导致术语的 nf（因此，导致术语的 nf）时，一个术语强规范化。强规范化术语的计算模拟是在计算的每个分支上终止的（非确定性）程序，而至少在一个分支上终止类似于弱规范化。
规范化的重要性引发了一系列问题（以及广泛的答案文献）。规约步骤的顺序（即规约策略）如何影响找到 nf（如果存在）？是否有组合基础可以保证每个组合器在该基础上存在正常形式？为了快速说明我们样本问题的可能答案，我们首先注意到，如果基础中没有具有重复效应的组合器，则该基础上的所有组合器都强规范化。这是一个非常简单的答案，作为一个具体的基础，我们可以选择{B,C,K}或{B,C,I}，由于它们与简单类型演算的关联而具有一些独立的兴趣。然而，这些基础远未达到组合完备性，甚至在其中无法定义不动点组合器。
我们可以提出一个稍微不同的问题：如果我们从基础{S，K}开始，省略 S，那么我们得到基础{K}，并且所有的组合子都强正规化，但是如果我们省略 K 呢？组合子{S}是否强正规化或者至少正规化？答案是“不”。一个术语（由 Henk Barendregt 在 20 世纪 70 年代初发现）显示了强正规化的缺乏，即 SSS（SSS）（SSS）。第一个 S 是一个（确实是唯一的）约简的头部，而这个术语的头部约简序列是无限的。由于{S}不包含任何具有可取消效应的组合子，一个术语存在无限约简序列意味着该术语没有 nf。在基础{S}上还有更短的组合子没有 nf，例如，S（SS）SSSSS 只包含八个 S 的出现。
我们在这里展示的问题类型（或者更确切地说，它们的答案）可能会变得有点技术性，因为它们经常涉及图论、自动机理论和术语重写理论的概念和技术。
2.3 固定点的存在和组合完备性
Schönfinkel 证明了 S 和 K 足以定义他引入的其他组合子，并且我们在 CL▹ 的定义中提到常量集仅限于 S 和 K，因为其他组合子可以从这些组合子中定义出来。
为了展示这里所理解的可定义性的意义，我们考虑 B 的例子。B 的公理是 Bxyz▹1x(yz)，如果我们用 S(KS)K 代替 B，那么将得到以下的规约序列。
S(KS)Kxyz▹1KSx(Kx)yz▹1S(Kx)yz▹1Kxz(yz)▹1x(yz)
术语 S(KS)K 是在正规形式中，然而，处于正规形式并不是可定义性的要求。使用处于正规形式的定义术语更加方便，因为对于不处于正规形式的组合子的应用可以通过将组合子简化为其正规形式来开始。（此外，总是存在无限多个可以简化为一个组合子的组合子。）然而，请注意，选择处于正规形式的组合子的偏好并不意味着一个组合子不能由两个或更多处于正规形式的术语来定义；下面我们给出了两个关于 I 的定义（仅涉及 S 和 K）。
如果常量是 S 和 K，那么组合子就是由 S 和 K（不包含变量）组成的所有术语。一旦我们将 B 定义为 S(KS)K，我们可以在进一步的定义中使用 B 作为缩写，我们这样做主要是为了减小结果术语的大小以及保持定义的透明度。
以下列表给出了我们之前提到的其他众所周知的组合子的定义。（这里，“=”被放置在被定义的术语和定义的术语之间。）
| I=SK(KK) | T=B(SI)K | C=B(T(BBT))(BBT) |
|---|---|---|
W=CSI | M=SII | Y=BW(BB′M)(BW(BB′M)) |
V=BCT | B′=CB | J=W(BC(B(B(BC))(B(BB)(BB)))) |
这些定义很容易看出所有这些组合子都依赖于 S 和 K，但从这些定义中并不明显得出这些定义的组合子是相互独立的，也就是说，没有一个列出的组合子可以从另一个组合子中定义出来。（显然，某些子集足以定义某些组合子。）我们不打算给出这些组合子各个子集之间的互定义的详尽列表，而是暗示这些定义的多样性和复杂性，我们列出其中一些。我们还引入了两个额外的组合子 S'和 R。
| I=SKK | I=WK | I=CK(KK) |
|---|---|---|
B=CB′ | S′=CS | S=CS′ |
W=S′I | W=B(T(BM(BBT)))(BBT) | W=C(S(CC)(CC)) |
R=BBT | Y=BM(CBM) | Y=B′(B′M)M |
如果不将固定点组合子 Y 视为原始的话，那么有多种方式来定义它——到目前为止，我们已经列出了三种。
固定点定理。对于任何函数 M，存在一个术语 N 使得 MN=N。
这个定理的证明很容易使用固定点组合子，因为一个可以扮演 N 的角色的术语是 YM。
Y 的一些定义在减少方面具有稍微不同的属性。但是固定点组合子的重要性在于它确保所有函数都有一个固定点，并且所有递归方程都可以解决。
哈斯凯尔·B·柯里（Haskell B. Curry）和艾伦·图灵（Alan Turing）都定义了固定点组合子（在 CL 或 λ 演算中）。如果我们考虑这些定义
Y1=BM(BWB)Y2=W(B(BW(BT)))(W(B(BW(BT))))
（其中下标是为了区分这两个定义），那么我们可以看到 Y1M=M(Y1M)，但对于 Y2，Y2M▹M(Y2M)也成立。在这方面，Y1 类似于 Curry 的不动点组合子（实际上，类似于任何不动点组合子），而 Y2 则类似于 Turing 的不动点组合子。
不动点定理在一定程度上展示了 CL 的表达能力。然而，不动点组合子可以从没有可消去元素的基础上定义（如 Y1 和 Y2 所示）。CL 的全部能力（以基础{S,K}）由以下定理阐述。
定理。（组合完备性）如果 f(x1,…,xn)=M（其中 M 是一个只包含显式列出的变量的项），那么存在一个组合子 X，使得 Xx1…xn 规约为 M。
定理的假设可以加强，排除了一些 x 的出现不在 M 中的可能性。然后，通过添加限定条件，可以加强结论，即 X 是一个相关的组合子，更具体地说，X 是一个在{B,W,C,I}上的组合子（不包含具有可取消效应的组合子的基础），或者等价地，X 是一个在{I,J}上的组合子（这些基础对应于 Church 首选的 λI-演算）。
组合完备性通常是通过在 CL 中定义一个“伪”λ-抽象（或括号抽象）来证明的。有各种算法可以在 CL 中定义一个括号抽象运算符，它的行为类似于 λ 运算符在 λ-演算中的行为。这个运算符通常用 [] 或 λ∗ 表示。这些算法在以下几个方面有所不同：（i）它们预设的组合子集合，（ii）生成的术语的长度，（iii）它们是否与将组合术语转换为 λ 术语的算法组合成（语法）恒等式，以及（iv）它们是否与任一规约或等式相互交换。
第一个算法的元素可能已经在 Schönfinkel（1924）中找到，它由以下按照列表顺序应用的子句组成。
(k)(i)(η)(b)(c)(s)[x].M=KM，其中 x∉fv(M)[x].x=I [x].Mx=M，其中 x∉fv(M)[x].MN=BM([x].N)，其中 x∉fv(M)[x].MN=C([x].M)N，其中 x∉fv(N)[x].MN=S([x].M)([x].N)
例如，如果将此算法应用于术语 λxyz.x(yz)（即 B 的 λ-翻译），则结果术语为 B。然而，如果省略 η，则结果术语会变得更长，即 C(BB(BBI))(C(BBI)I)。例如，另一个算法由子句(i)、(k)和(s)组成。
3. 非经典逻辑和类型化组合逻辑
3.1 简单类型
组合术语被视为函数，而函数被认为具有一个定义域（可能输入的集合）和一个值域（可能输出的集合）。例如，如果将一元函数视为有序对的集合，则定义域和值域分别由第一个和第二个投影给出。如果允许部分和非满射函数，则第一个和第二个投影得到的集合的超集也可以是定义域和值域。范畴论中，函数是范畴的组成部分（不假设集合论的约简），保留了定义域和值域的概念；此外，每个函数都有唯一的定义域和值域。
然而，具有相同定义域和值域的函数可能非常不同，但通过抽象，它们属于相同的类型。作为一个简单的例子，设 f1 和 f2 是定义为 f1=λx.8⋅x 和 f2=λx.x/3 的两个函数。如果 x 是一个变量，范围是实数，则 f1 和 f2 具有相同的定义域和值域（即它们具有相同的类型 R→R），尽管 f1≠f2，因为只要 x≠0，就有 f1(x)≠f2(x)。表示函数 f 的定义域为 A，值域为 B 的通常符号是 f:A→B。现在‘→’通常在逻辑学中用作蕴涵或（非经典的）蕴涵的符号，这是一个巧合。
给定一组基本类型（我们用 P 表示），类型定义如下。
如果 p∈P，则 p 是一个类型；
如果 A、B 是类型，则(A→B)是一个类型。
为了将这些类型与其他类型区分开来——其中一些在下一节中介绍——它们被称为简单类型。
组合子与类型之间的关系可以通过身份组合子的例子来解释。复合组合术语是通过应用操作形成的。假设推理的前提可以通过融合（用 ∘ 表示）来连接，这类似于最强关联逻辑 B 中的应用操作。如果 Ix▹x，那么如果 x 的类型是 A，那么 Ix 的类型应该蕴含 A。此外，Ix 的类型应该是 X∘A 的形式，其中 X 是某种类型；那么 Ix 可以是 A→A 的类型。在这个例子中，我们固定了 x 的类型，然而，Ix 可以应用于任何术语，因此更准确地说，A→A 是 I 的类型模式，或者说 I 的类型可以是任何自我蕴涵形式的公式。
类型分配系统 TACL 被正式定义为以下推导系统。（当将蕴涵公式视为类型时，通常的约定是通过与右侧的关联来省略括号。）
Δ⊢S:(A→B→C)→(A→B)→A→CΔ⊢K:A→B→AΔ⊢M:A→BΘ⊢N:AΔ,Θ⊢MN:B
形如 M:A 的表达式被称为类型赋值。类型赋值系统的一个特征是，如果 M:A 是可证明的，则 A 被认为是可以分配给 M 的类型之一。然而，可证明的赋值并不排除其他类型与同一术语 M 相关联，即类型赋值并不能固定术语的类型。⊢ 左侧的 Δ 和 Θ 是变量的类型赋值集合，它们被假定是一致的——意味着一个变量不能被分配两个或更多的类型。
类型赋值系统通常被称为 Curry 风格的类型系统。另一种为术语分配类型的方法是为每个术语固定一个类型，这样每个术语就有且仅有一个类型。这样的演算被称为 Church 风格的类型系统。例如，类型为
(A→A→A)→A→A→A
不同于类型为 I 的恒等组合子 I
((B→B)→B)→(B→B)→B.
两种打字风格在很多方面有相似之处，但它们之间也存在一些差异。特别是，在 Church 风格的打字系统中，无法对自我应用进行打字，而在 Curry 风格的打字系统中，可以为其中一些术语分配类型。Curry 风格的打字系统在建立 CL 和 λ-演算的各种属性方面非常有用。另一方面，Church 风格的打字更接近某些函数式编程语言（不包含对象）的打字。
在任何一种打字风格中，类型和组合子之间没有一一对应的关系：并非所有的组合子都可以分配一个类型，而且一些蕴涵公式无法分配给任何组合子术语。可以分配一个类型的组合子被称为可打字的，可以分配给组合子的类型被称为有居住性的。例如，M 没有（简单的）类型，因为蕴涵公式永远不等于其自身的前提。另一方面，皮尔斯定律，((A→B)→A)→A，在类型分配系统 TACL 中不是任何组合子的类型。尽管蕴涵公式和组合子术语之间存在差异（或者说正是由于这种差异），可以分配给某些组合子术语集合的蕴涵公式类与一些重要逻辑的定理集合相一致。
定理。A→B 是直觉蕴涵逻辑的一个定理，用 IPC→或 J→表示，当且仅当存在某个 M，M:A→B 是 TACL 中可证明的类型分配，其中术语 M 是由 S 和 K 构建的，即 M 是基础集合{S,K}上的组合子。
一个存在于蕴含定理中的组合子在 TACL 推导系统中编码了该定理的证明。有一种算法可以恢复组合子类型的证明构成的公式，此外，该算法产生的证明是最小和良构的。直觉逻辑的蕴含定理（及其证明）与可类型化的闭合 λ-项（或组合子）之间的对应关系被称为 Curry-Howard 同构。在 Hilbert 样式公理系统中，证明的通常概念相当宽松，但可以整理得到遍历证明的概念。在遍历证明中，组合子的子项与遍历证明中的公式之间以及应用和分离之间存在一一对应关系（参见 Bimbó 2007）。
上述对应关系可以修改为其他蕴含逻辑和组合基础。下面的定理列出了在相关逻辑 R 和 T 的蕴含片段与一些本身具有兴趣的组合基础之间获得的对应关系。
定理。A→B 是 R→（或 T→）的一个定理，当且仅当存在某个 M，M:A→B 是一个可证明的类型赋值，其中 M 是一个在{B，I，W，C}上的组合子（或在{B，B'，I，S，S'}上的组合子）。
通过为两个基础中的组合子添加公理模式，可以修正演算 TACL。（这些基础中不包含的组合子的公理模式可以从演算中省略，或者在证明中可以忽略。）新的公理如下。
B：（A→B）→（C→A）→C→BB'：（A→B）→（B→C）→A→CC：（A→B→C）→B→A→CW：（A→A→B）→A→BS'：（A→B）→（A→B→C）→A→CI：A→A
组合基础{B，C，W，I}特别有趣，因为这些组合子足以定义等同于 λI 演算的括号抽象。（换句话说，所有依赖于其所有参数的函数都可以通过这个基础来定义。）另一个基础允许定义可以由所谓的遗传右极大项类别中的术语描述的函数（参见 Bimbó 2005）。非正式地说，这些术语背后的思想是函数可以被枚举，然后它们的连续应用应该形成一个序列，其中索引“全局增加”。
类型赋值有两个部分：一个术语和一个公式。某个术语是否可以被赋予一个类型，以及某个类型是否可以被赋予一个术语，这些问题分别是可赋型和居住性的问题。尽管这些问题可以针对同一组类型赋值进行提出，但这些问题的计算特性可能有很大的差异。
定理。判断一个术语 M 是否可以被赋予一个类型，即 M 是否可赋型，是可判定的。
这个定理以一种相当一般的方式陈述，没有明确指定使用哪个组合基础或 TACL 的哪种修改，因为该定理适用于任何组合基础。实际上，存在一个算法，可以在给定一个组合子的情况下判断该组合子是否可赋型，并为可赋型的组合子生成一个类型。当然，在组合完备基础{S,K}中，所有的组合子都可以表示为仅由这两个组合子组成的术语。然而，这个假设对于可赋型的解决方案并不是必需的，尽管它可能为存在一个通用算法提供了一个解释。
居住问题没有类似的通解，因为组合术语的相等性问题是不可判定的。给定一组公理模式，它们是带有推理规则的组合子类型，逻辑的可判定性问题可以被视为居住问题。实际上，如果 A 是一个蕴含式公式，那么决定 A 是否是一个定理就等于确定是否存在一个术语（在与公理模式对应的基础上），可以将 A 分配为其类型。（当然，更复杂的算法可能实际上会产生这样的术语，在这种情况下，通过重建定理的证明来验证主张的正确性是很容易的。）
要看到在可判定性的情况下可能出现的复杂性，我们比较术语的形成规则和推理规则。给定一个组合基础和一个可数的变量集合，通过检查可以判定一个术语是否在生成的术语集合中。也就是说，规则的所有输入在输出中作为结果术语的子术语保留。相比之下，推理规则的应用会导致一个公式，它是主前提的一个真子公式（在主前提是自恒等的情况下，它与次前提相同）。通过应用演绎法则，不保留前提的所有子公式是导致蕴涵逻辑的一些决策问题困难的原因。因此，对于许多可判定的逻辑来说，存在一种使用序列演算的决策过程，其中割定理和子公式性质成立。居住问题的解决方案可能会遇到类似于一般可判定性问题的困难。
例如，组合子 K 可以被赋予以下类型。
p→(q→(q→q→q)→(q→q)→q→q)→p
SKK 可以被赋予类型 p→p。在 TACL 中有一个以 SKK:p→p 结尾的证明，该证明不包含上述长公式。然而，有一个包含上述公式的 SKK:p→p 的证明，其中第二个前提不是 p→p 的子公式，事实上，这两个公式的子公式集是不相交的。（我们选择了两个不同的命题变量 p 和 q 来强调这一点。）然而，问题的一些重要情况是可判定的。
定理。对于基础集合{S,K}，判断一个类型是否有一个元素是可判定的。
这个定理等同于直觉逻辑的蕴涵片段的可决定性的类型化版本，该版本是 Gentzen 的可决定性结果的一部分（追溯到 1935 年）。
定理。判断一个类型是否在基础集合{I,C,B′,W}上有一个元素是可决定的。
这个定理是相关蕴涵逻辑的蕴涵片段的可决定性的类型化等价物。Saul A. Kripke 在 1959 年证明了 R→的可决定性，同时也证明了与之密切相关的 E→（蕴涵逻辑的蕴涵片段）的可决定性。
定理。如果一个类型在基础集合{B，B'，I，W}上有一个元素，则它是可判定的。
这个定理是逻辑学中的蕴涵片段的可判定性的类型化版本，该定理与 Bimbó 和 Dunn（2012）以及 Bimbó 和 Dunn（2013）证明的 R→（带有真值常量 t 的 R→）和 Tt→（带有真值常量 t 的 T→）的可判定性一起证明。Padovani（2013）中有一个独立的结果（仅适用于 T→），它扩展了 Broda 等人（2004）的结果。
Tt→和 Rt→的决策过程不使用 TACL 或公理演算，而是建立在连续演算（即，连续演算中不假设结构连接是结合的）的基础上。结构规则和组合子之间存在亲和性的想法至少可以追溯到 Curry（1963）。为了加强这种联系，Dunn 和 Meyer（1997）引入了结构自由逻辑，其中组合子的引入规则取代了结构规则，因此这些逻辑被标记为结构自由逻辑。Bimbó 和 Dunn（2014）引入了一种从序列演算的标准证明中生成 T→定理的组合子元素的技术，该技术在 Tt→的决策过程中使用。序列演算比自然演绎或公理系统更好地控制证明过程。Bimbó 和 Dunn（2014）的组合子提取过程在序列演算证明中建立了组合子和类型之间的有效链接，从而消除了 TACL 和公理系统的明显优势。
替换规则是通过称为分离的规则模式和基本组合子的公理模式来内置到 TACL 的制定中的。很明显，存在最简复杂度的 S 和 K 类型的公式，所有其他类型的 S 和 K 都是它们的替换实例。具有这种属性的公式被称为组合子的主要类型。显然，具有主要类型的组合子具有可数无穷多个主要类型，它们都是彼此的替换实例；因此，可以谈论组合子的主要类型模式是合理的。复杂组合子的主要类型的存在并不明显，然而，确实存在。
定理。如果术语 M 是可类型化的，则 M 具有主要类型和主要类型模式。
现在，主要类型和主要类型模式似乎可以在任何地方互换使用。因此，我们可以采取稍微不同的方法，将 TACL 定义为包括公理和分离规则模式以及替换规则。这个版本的 TACL 将采用以下形式。
Δ⊢S:(p→q→s)→(p→q)→p→sΔ⊢K:q→s→qΔ⊢M:A→BΘ⊢N:AΔ,Θ⊢MN:BΔ⊢M:AΔ [P/B] ⊢M:A [P/B]
其中 P 代表命题变量。（替换符号的使用方式自然地扩展到类型赋值的集合。）显然，这两个推导系统是等价的。
如果完全放弃替换，那么演绎的适用性将变得极为有限，例如，SK 将不再可输入。在完全使用替换和完全不使用替换之间取得折中的方法是修改演绎规则，以包括尽可能多的替换，以确保演绎规则的适用性。这样的规则（不包括组合术语或类型赋值）在 1950 年代由 Carew A. Meredith 发明，通常称为简化演绎。演绎的适用性的关键是找到次前提和主前提的前件的共同替换实例。这一步骤称为统一。（稍微正式一些，让 s(A)表示将替换 s 应用于 A。那么，从 B→C 中简化演绎出的结果是 s(C)，当存在一个 s 使得 s(A)=s(B)，并且对于任何具有此属性的 s1，存在一个 s2 使得 s1 是 s 和 s2 的组合。）
注意，总是可以选择一对公式的替代实例，使得它们的命题变量集合不相交，因为公式是有限的对象。两个公式 A 和 B 的最一般的共同实例（它们不共享命题变量）是 C，其中 C 是 A 和 B 的替代实例，并且只有在必要时才通过替代来识别命题变量，以获得既是 A 的替代实例又是 B 的替代实例的公式。统一定理（针对简单类型）暗示，如果两个公式 A 和 B 有一个共同实例，则存在一个公式 C，使得 A 和 B 的所有共同实例都是 C 的替代实例。显然，一对公式要么根本没有共同实例，要么有 ℵ0 个最一般的共同实例。
一对没有共同实例的公式的著名例子是 A→A 和 A→A→B。实例 p→p 和 q→q→r 没有共享命题变量，然而，既不是 q→q 也不是(q→r)→q→r 与第二个公式的形状匹配。换句话说，q 和 q→r 必须被统一，但无论用什么公式替代 q，它们都无法被统一。这个问题的一个直接结果是 WI 不可类型化。
另一方面，
(r→r)→r→r
和
((s→s)→s→s)→(s→s)→s→s
是 p→p 和 q→q 的替换实例。此外，所有简单类型都是命题变量的替换实例，因此 II 可以被赋予类型 r→r 和类型(s→s)→s→s，当然，后者恰好是前者的实例，因为 A→A 是 II 的主要类型模式。如果我们将 p→p 和 q→q 应用于紧凑推断，那么我们得到 q→q（通过替换 [p/q→q] 和 [q/q]），因此紧凑推断产生了 II 的主要类型。顺便说一句，II 和 I 提供了一个很好的例子，说明不同的术语可能具有相同的主要类型模式。
紧凑推断已广泛用于改进各种蕴涵逻辑的公理化，尤其是在寻找更短和更少的公理方面。一些逻辑可以使用公理（而不是公理模式）以及紧凑推断规则来表述，而不会丧失定理。到目前为止，我们提到的所有逻辑（J→，R→，T→和 E→）都是 D-完备的，也就是说，它们都可以通过公理和紧凑推断规则来公理化。也就是说，经典逻辑和直觉逻辑的蕴涵片段，以及相关逻辑 R、E 和 T 的蕴涵片段都是 D-完备的。（有关一些进一步的技术细节，请参见 Bimbó（2007）。）
简单类型系统已经在各个方向上得到了扩展。逻辑通常包含除了蕴涵之外的连接词。将类型分配系统通过包含进一步的类型构造器来扩展类型集合是一种自然的修改。合取和融合是最容易解释或激励作为类型构造器的方式，然而，析取和逆向蕴涵也被引入到类型中。类型是有用的，因为它们允许我们从归约的角度把握术语类的行为。
泰特定理。如果一个组合术语 M 是可类型化的（具有简单类型），那么 M 是强正规化的，也就是说，M 的所有规约序列都是有限的（即终止）。
这个主张的逆命题显然是不成立的。例如，WI 是强正规化的，但是不可类型化，因为收缩的前提不能与任何自涵实例统一。扩展可类型化术语集合的目标导致了 ∧ 在类型中的引入。
3.2 交集类型
以不同的方式看待键入 WI 的问题是说 W 应该具有类似于(A→(A→B))→A→B 的公式的类型，但在前提中，以 A 和 A→B 替代的公式可以统一。这是将合取(∧)和顶(⊤)作为新的类型构造器包含的动机。
扩展类型系统，通常称为交集类型学科，归功于 Mario Coppo 和 Mariangiola Dezani-Ciancaglini。交集类型的集合（用 wff 表示）定义如下。
如果 p 是命题变量，则 p∈wff。
⊤∈wff，其中 ⊤ 是一个常量命题；
A,B∈wff 意味着(A→B),(A∧B)∈wff。
当然，如果 TACL 与一个扩展的类型集合相结合，那么之前分配的类型的新实例将变得可用。然而，拥有新的类型构造符 ∧ 和 ⊤ 的类型的要点是，类型集合具有比由替换规则和推理规则确定的类型之间的关系更丰富的结构。
交集类型的结构由 B 的合取-蕴涵片段描述，即基本相关逻辑。在下面对这个逻辑的介绍中，≤ 是公式的主要联结词（蕴涵），⇒ 分隔前提和推理规则的结论。
A≤AA≤⊤⊤≤⊤→⊤A≤A∧AA∧B≤AA∧B≤BA≤B,B≤C⇒A≤CA≤B,C≤D⇒A∧C≤B∧D(A→B)∧(A→C)≤(A→(B∧C))A≤B,C≤D⇒B→C≤A→D
组合子 S、K 和 I 的公理模式如下。请注意，S 的公理不仅仅是前一个 S 的公理的替换实例（包括新的联结词）。
Δ⊢S:(A→B→C)→(D→B)→(A∧D)→CΔ⊢K:A→B→AΔ⊢I:A→A
有四个新规则被添加，并且有一个关于 ⊤ 的公理。
Δ⊢M:AΔ⊢M:BΔ⊢M:A∧BΔ⊢M:A∧BΔ⊢M:AΔ⊢M:A∧BΔ⊢M:BΔ⊢M:AA≤BBΔ⊢M:BΔ⊢M:⊤
这种类型赋值系统等同于 λ 演算的交集类型赋值系统，并且它允许更精确地描述与规约序列的终止相关的术语类别。
定理。 （1）当 M 可类型化时，术语 M 归一化。 (2) 一个术语 M 在 M 可输入且证明不包含 ⊤ 时强正规化。
4. 模型
CL 有各种模型，其中三种在本节中详细说明。代数模型（通常称为“术语模型”）可以轻松构建，适用于在第 2.1 节中介绍的 CL 的不等式系统和等式系统。术语集构成一个代数，给定一个适当的等价关系（也是一个同余关系），应用操作可以按照标准方式提升到术语的等价类。所得代数的准不等式特征为这些逻辑提供了代数语义的基础。隔离 Lindenbaum 代数并验证它不是一个平凡代数构成了 CL▹ 和 CL=的一致性证明。
4.1 斯科特的模型
Dana Scott 为 λ 演算定义了 Pω 和 D∞。我们首先概述 Pω——所谓的图模型，这更容易理解。
自然数具有非常丰富的结构。Pω 是自然数集的幂集，它是与相同标签的模型的核心。每个自然数在二进制中有唯一的表示。（例如，710 是 111，即 7=1⋅22+1⋅21+1⋅20=4+2+1。）每个二进制表示的形式为
bm⋅2m+bm−1⋅2m−1+⋯+b1⋅21+b0⋅20，
其中每个 b 都是 0 或 1。然后，每个二进制数可以被视为自然数有限子集的特征函数。（在左边，有无限多个零，如…000111，被省略。）对于自然数 n，en 表示相应的自然数有限集。（例如，e7={0,1,2}。）
Pω 上的正拓扑包括有限生成的开集。设 E 表示 ω 的有限子集。X⊆Pω 是开集，当且仅当 X 是由 E 的子集生成的锥体（相对于 ⊆）。给定正拓扑，函数 f:Pω→Pω 在通常的拓扑意义下连续，当且仅当 f(x)=∪{f(en):en⊆x}，其中 en∈E。这意味着 m∈f(x)当且仅当 ∃en⊆x.m∈f(en)，这导致了函数 f 通过自然数对（n,m）的表征。
通过自然数和自然数的（有序）对之间的一一对应，定义了一个关系
(n,m)=[(n+m)⋅(n+m+1)]+2⋅m2
构成（一元）函数的对的集合有时被称为函数的图。连续函数 f:Pω→Pω 的图由 graph(f)={(n,m):m∈f(en)}定义。为了能够建模无类型应用，包括自我应用，ω 的子集也应被视为函数。对于 x,y⊆ω，由 y 确定的函数被定义为 fun(y)(x)={m:∃en⊆x.(n,m)∈y}。对于连续函数 f，fun(graph(f))=f 成立。
CL 的图模型将术语映射到 ω 的子集。首先，组合子具有具体集合作为它们的解释。作为一个简单的例子，I={(n,m):m∈en}。当然，每对对应于 ω 的一个元素，因此我们得到了一组自然数。特别地，其中一些元素是{1,6,7,11,15,23,29,30,…}。
如果将组合子（以及变量）解释为 ω 的子集，则函数应用应该将第一个集合（视为类型 Pω→Pω 的函数）应用于第二个集合。fun(y)是一个适当的函数，由 y⊆ω 确定。一般来说，如果 M 和 N 是 CL 术语，I 是将原子术语解释为 Pω 的解释，则通过 I(MN)=fun(I(M))(I(N))将 I 扩展为复合术语。（例如，让 I(x)为 e9={0,3}。I(Ix)=fun(I(I))(I(x))={m:∃en⊆I(x).(n,m)∈I(I)}。我们知道 I(I)和 I(x)是什么；因此，我们进一步得到 I(Ix)={m:∃en⊆e9.m∈en}。当然，{0,3}⊆{0,3}，所以我们有 I(Ix)={0,3}。）这个模型支持一种内涵的函数概念。
作为一个函数空间的无类型应用系统的最早模型也是在 60 年代末由斯科特提出的，比图模型早了几年。以下是构建过程的一些关键要素的概述。
在纯类型无关的逻辑学中，形如 MM 的表达式是一个良构的术语。此外，这种形式的术语可以以多种方式进入可证明的方程和不等式中。例如，xx=xx 是一个公理，而根据其中一条规则，y(xx)=y(xx)也是可证明的。形如 MM 的术语的一个更有趣的出现可以在可证明的不等式 S(SKK)(SKK)x▹xx 中看到。
函数的集合论约简产生一组对（一般来说，是一组元组）的集合。在集合论中（当然，假设良基性），一对（例如，{{a},{a,b}}）永远不等于其两个元素之一。因此，关于 CL 的数学模型的主要问题是如何处理自我应用。
Scott 的原始模型是从一个完备格（D,≤）开始构建的。也就是说，（D,≤）是一个偏序集，在其中对于任意元素集合，存在最大下界（infima）和最小上界（suprema）。当函数 f 从（D,≤）到一个完备格（E,≤）时，如果它保持 D 上每个理想的上确界，其中理想是一个向上有向的下闭子集，那么它被称为连续的。
拓扑可以通过选择某些递增集合作为开集来定义在 D 上。更准确地说，如果 I 是一个理想，C 是一个锥体，那么当且仅当 C∩I≠∅ 时，C 是开集，前提是 ⋁I∈C，也就是说，I 的上确界是 C 的一个元素。（例如，主理想的补集是开集。）当 D 和 E 与它们的拓扑一起考虑时，f 在通常的拓扑意义下是连续的，也就是说，开集的逆像是开集。这解释了之前将这些函数标记为连续的原因。值得注意的是，所有连续函数都是单调的。
为了在 CL 中对函数进行建模，有趣的函数是在 D 上连续的函数。然而，这些函数本身并不足以获得自我应用的建模，因为它们中没有一个的定义域是函数集合，因为没有假设 D 是一个函数空间。解决方案是从定义一系列函数空间 D0，D1，D2，...开始，使得每个函数空间 Dn 都是一个完备格，可以在其中定义连续函数（创建函数空间 Dn+1）。选择连续函数的重要性在于新出现的函数空间与底层集合具有相同的基数，这使我们能够定义在层次结构中相邻的函数空间之间的嵌入。
所有函数空间 Dn 的层次结构可以累积在一起。模型论中的一个标准构造是形成结构的不相交并集。（通过对结构的载体集进行索引，可以始终保证不相交。）Scott 将 D∞ 定义为函数空间 Dn 的不相交并集，其中 n 为所有 n，除了极端元素被“粘合在一起”。（更正式地说，函数空间的顶部元素和底部元素分别与彼此相同。）D∞ 是一个完全格，根据塔斯基的不动点定理，将 D∞ 映射到 D∞ 的连续函数具有一个不动点，这意味着 D∞ 与 D∞→D∞ 同构。
上述构造也可以用字符串和笛卡尔积的概念来理解。在一元函数和多元函数之间的来回移动——函数的“展开”和“收缩”——在代数上对应于两个方向的残余。例如，函数 f：A×B→C 可以由函数 f'：A→B→C 表示，反之亦然。因此，不失一般性，只需考虑一元函数即可。如果 a 是函数空间 D∞ 的固定元素，则当 x 是 a 的不动点时，x=(a,x)成立。从元组的角度来看，解可以被视为无限元组(a,(a,(a，…
4.2 关系语义
我们简要概述的另一个模型属于非经典逻辑的集合论语义范式，这归功于 J. Michael Dunn 和 Robert K. Meyer（参见 Dunn 和 Meyer（1997））。CL 和 λ 演算与直觉主义、相关性和其他非经典逻辑有着内在联系。特别地，CL▹ 和 CL=演算本身就是非经典逻辑。自 20 世纪 60 年代初以来，集合论语义一直是非经典逻辑的首选解释，其中内涵连词是从一组情境上的关系建模的。这种语义有时被称为“Kripke 语义”（因为 Kripke 在 1959 年为一些正常的模态逻辑引入了可能世界语义）或“gaggle 语义”（根据 Dunn（1991）引入的缩写“ggl”的发音，代表“广义 Galois 逻辑”）。
对于 CL▹，可以定义如下模型。让(W,≤,R,S,K,v)组成一个（非空）偏序集(W,≤)，其中 W 上有一个三元关系 R，并且 S、K∈W。此外，对于任意的 α、β、γ、δ∈W，条件(s)和(k)成立。
(s)∃ζ1,ζ2,ζ3∈W.RSαζ1∧Rζ1βζ2∧Rζ2γδ 蕴含 ∃ζ1,ζ2,ζ3∈W.Rαγζ1∧Rβγζ2∧Rζ1ζ2δ,
(k)∃ζ1∈W.RKαζ1∧Rζ1βγ 意味着 α≤γ。
三元关系被规定为在其前两个参数位置上是反单调的，在第三个参数位置上是单调的。这些组成部分为 CL▹ 定义了一个框架。估值函数 v 将变量 x、y、z 等映射到 W 上的（非空）锥体，并将两个原始组合子 S 和 K 分别映射到由 S 和 K 生成的锥体。请记住，CL 中的标准符号隐藏了应用，这是一种允许形成复合术语的二元操作。下一个子句将 v 扩展到复合术语，并再次明确了这个操作。
v(MN)={β:∃α,γ.Rαγβ∧α∈v(M)∧γ∈v(N)}
一个不等式 M▹N 在 CL▹ 的所有帧的估值下，如果 v(M)⊆v(N) 成立，则该不等式是有效的。（也就是说，无论在变量集上如何变化，两个术语的解释之间的关系是不变的。）
非正式地说，底层集合 W 是一组情境的集合，R 是连接情境的可达关系。所有术语都被解释为情境的集合，并且函数应用是从 R 派生的存在性映像操作。与之前的模型不同的是，一个术语对另一个术语的应用的结果不是由解释这两个术语的对象本身决定的，而是应用操作是从 R 定义的。
这种语义学推广了普通模态逻辑的可能世界语义学。因此，重要的是要注意，这些情境不是最大一致理论，而是具有以下性质的理论：对于任意一对公式，它们都包含一个蕴含这两个公式的公式。等价地，这些情境可以被视为 CL▹ 的林登鲍姆代数上的对偶理想。这些情境通常在某种意义上是一致的，即它们不包含除一个例外之外的所有术语。（当然，否定一致性的概念无法为 CL▹ 或 CL=定义。）
对于 CL=，可以沿着类似的思路定义关系语义。然后，得到了声音性和完备性，即以下定理：
定理。 (1) 在 CL▹ 中，当且仅当对于 CL▹ 的任何模型中 v(M)⊆v(N)，不等式 M▹N 是可证的。 (2) 在 CL=中，当且仅当对于 CL=的任何模型中 v(M)=v(N)，方程 M=N 是可证的。
关于包括双重和对称组合子的 CL 系统的关系和操作语义可以在 Bimbó（2004）中找到。
5. 可计算函数和算术
CL 的一个显著特点是，尽管它看起来很简单，但它是一个强大的形式化工具。当然，如果没有发现组合术语之间的某些关系，或者没有一个可计算函数可定义的示例，就无法欣赏到 CL 的强大之处。
数学形式化的一个重要起步步骤是对算术进行形式化，这是由 Dedekind-Peano 公理化首次实现的。在 CL 中，有多种形式化算术的方法；本节将介绍两种数字表示以及一些与之相关的函数。
数字可以被认为是某种对象（或抽象对象）。 （在这里，我们所指的数字是自然数，即 0 和正整数。）数字可以通过它们作为集合所具有的结构来进行描述。这种结构支持诸如 0≠1 以及 n 和 m 的和与 m 和 n 的和相同的性质。自然数的另一个众所周知的性质是，例如，存在无限多个素数。
数字可以用术语在 CL 中表示，一种方法是选择术语 KI，I，SBI，SB（SBI），…表示 0，1，2，3 等。表示算术运算的术语因所代表的数字而异。请注意，与 Dedekind-Peano 算术的形式化不同，CL 没有进行语法区分，以使其与个体常量和函数符号之间的差异相对应-在 CL 中，唯一的对象是术语。上述术语列表已经显示了后继函数，即 SB。（SB（KI）等于 I，即 1 是 0 的后继。）
加法术语是 BS（BB），乘法术语是 B。基于加法的通常递归定义可能暗示加法应该是比乘法更简单的操作。然而，在 CL 中，数字本身就是函数，因此它们具有使 B（一个看起来更简单的术语）被选择为通常被认为比加法更复杂的函数的属性。（可以使用原始递归来定义加法运算，这将产生一个更复杂的术语。）作为一个经典的例子，我们可以考虑术语 BII，它与 I 强相等，即 1×1=1-正如预期的那样。我们在这里不进一步探讨这种数字表示法。我们只注意到这些数字的形状与 λ-演算中的 Church 数密切相关，其中每个数字都是一个二元函数（而这里，每个数字都是一个一元函数）。
用另一种方式在 CL 中表示数字的方法是从数字的不同选择开始。以前，我代表 1，现在我们将 I 作为 0。数字 n 的后继是 V(KI)n，其中 n 的第二次出现表示一个数字，即表示 n 的组合子。（表示 n 的数字通常用有上划线或其他装饰的 n 来表示，但在有限的上下文中 n 的双重使用不应引起任何混淆。）换句话说，后继函数是 V(KI)。请注意，当前表示中的数字是在比以前情况下更受限制的组合基础上的术语。例如，从{I,K,V}中无法定义具有重复效果的组合子。
一些简单的递归函数可以如下定义。对于大于或等于 1 的所有数字，前驱函数 P 是“-1”（即减去一），而 0 的前驱被设置为 0。下一个术语定义了前驱函数，它被缩写为 P。
P=C(W(BB(C(TK)I)))(KI)
如果 n 是一个数字，那么 Pn 会简化为 nKI(n(KI))，这表明对于正数，P 可以被定义为术语 T(KI)，因为只要 n 是形式为 V(KI)(n-1)的术语，T(KI)n 会简化为 n-1。
一些计算模型（如寄存器机器）和某些编程语言包括对零的测试作为原始构造。找到一个 CL 术语来表示函数 Z 是有用的，使得当 n 为零时，Znxy 简化为 x，而当 n 为正数时，Znxy 简化为 y。可以将 Znxy 视为条件指令“如果 n=0，则 x，否则 y”，其中 x 和 y 本身就是函数。（当然，在伪代码中应该假设 n 是整数类型且不能取负值，这可以通过变量声明和额外的条件语句来保证。）以下定义适用于零分支。
Z=TK
TKnxy=nKxy，如果 n 为零，即 n=I，则通过另一步 Kxy 然后得到 x 的结果；而如果 n 为正数，则经过几次规约后，得到 KIxy，即 y。这两个术语，Kxy 和 KIxy，暗示了将 K 和 KI 解释为真和假，或者可以将它们视为可以选择第一个或第二个参数的术语。这些想法可以进一步发展为真值函数的定义和元组的表示。
加法可以通过递归方程+mn=Zmn(V(KI)(+(Pm)n))来定义，其中 m 和 n 是数字，P 和 Z 是已定义的函数。（缩写用于增强术语的可读性，可以在任何地方用定义的组合子替换它们。）换言之，如果 m 为 0，则和为 n，否则 m+n 是(m-1)+n 的后继。当然，这个定义密切模拟了递归理论中的加法定义，其中加法通常由两个方程+(0,n)=n 和+(s(m),n)=s(+(m,n))（其中 s 表示后继函数）定义。CL 能够以这种形式表达加法的事实再次显示了 CL 的多功能性。
组合完备性保证了定义+的方程右侧的术语（即术语 Zmn(V(KI)(+(Pm)n)））可以转化为一个术语，其中+是第一个参数，m 和 n 分别是第二个和第三个参数。然后，可以将+明确地定义为组合子的不动点。
B(BW)(BW(B(B(C(BB(BC(TK)))))(B(B(B(V(KI))))(CB(T(KI)))))).
当然，为了透明起见，我们可以将得到的术语缩写为+，就像我们之前使用 P 和 Z 作为更长的组合术语的简写一样。
乘法通常用 ⋅ 表示。递归方程 ⋅mn=ZmI(+n(⋅(Pm)n))定义了乘法，可以解释为“如果 m 为 0，则结果为 0，否则将 n 添加到(m−1)⋅n 的结果中”。定义的下一步将右侧术语转化为 X⋅mn 的形式，其中 X 不包含 ⋅、m 或 n 的出现。然后取 X 的不动点，并将 ⋅ 设置为 YX，从而完成了乘法函数的定义。例如，抽象可以产生组合子。
BW(B(B(C(BB(C(TK)I))))(B(BW)(B(B(B(C+)))(CB(T(KI)))))).
阶乘函数可以从前驱函数和乘法中定义，并且在组合学中非常有用。阶乘函数（表示为！）可以通过方程！m=Zm(V(KI)I)(⋅m(!(Pm)))递归地定义，可以理解为“如果 m 为 0，则！m=1，否则！m 等于 m 乘以 m-1 的阶乘。”
当然，没有必要通过模拟递归定义来定义各种数值函数。正如我们在数字的第一种表示中所看到的，我们可能刚好有正确的术语，如 BS（BB）和 B，它们在数字上的行为与目标函数相同。也就是说，定义算术函数的另一种好方法是简单地列出一些术语，然后展示它们的行为与预期相符。然而，一旦已经证明了基本的原始递归函数连同递归和最小化可以在逻辑学中模拟，我们不仅得到了一组很好的用于工作的组合子形式的算术函数，而且还证明了组合逻辑足够表达所有的部分递归函数。实际上，这样一个证明的剩余步骤可以在逻辑学中完成，尽管细节超出了本条目的范围。
5.1 哥德尔句子
在上述草图中，缩写词和插入的解释可能会掩盖算术已经以由五个符号组成的语言进行形式化的事实（不计算并置）。这五个符号是：S、K、=，加上两个分隔符（（和））。有限（也许是令人惊讶地少）的符号数量和递归函数的可用性使人想到可以尝试对 CL 的语法进行算术化。
哥德尔通过给符号、公式和公式序列分配数字来实现对形式语言的编码，后来被称为“哥德尔数”。具体而言，哥德尔将奇数分配给符号，将质数的幂的乘积（其中数字对应于指数中的符号）分配给符号序列。然而，可以在不过分强调质数的存在和性质的情况下对 CL 的语言进行算术化。（例如，参见雷蒙德·M·斯穆利安的书籍：斯穆利安（1985）和斯穆利安（1994）。）这五个符号的哥德尔数分别为前五个正整数。字符串被分配一个十进制数，该数是由相应符号的数字连接而成。
下面的概述呈现了适用于 CL 的哥德尔不完备性定理的类比。可以定义一个组合子，使得如果将该组合子应用于数字 n，则整个术语将简化为表示数字 n 的哥德尔数的数字 m。稍微正式一点说，存在一个组合子 δ，使得 δn=G(n)（其中 G(n)表示表达式 n 的哥德尔数）。此外，存在一个组合术语，当应用于数字 n 时，返回数字本身后跟 G(n)。对于任何术语 A，存在一个术语 B，使得方程 A(δB)=B 成立。这个陈述（或其特定形式适用于特定形式系统）通常被称为第二个不动点定理。递归数集的可计算特征函数可以用选择 K 表示真值和 KI 表示假值的组合子来表示。这些函数的补集也是可计算的。最后，可以证明不存在一个代表所有真等式的组合子。换句话说，任何组合子要么代表一个不包含某些真等式的等式集，要么代表一个包含所有真等式但也包含一些假等式的等式集。
阿隆佐·邱奇依靠哥德尔的不完备性定理证明了经典一阶逻辑的不可判定性。达纳·斯科特证明了如果 A 是一个在等式下封闭的非空真子集，则 A 不是递归的。对于 CL 来说，由于存在一个 CL 的哥德尔句子，类似的主张是判断两个 CL 术语是否相等是不可判定的。
Bibliography
Due to obvious limitations of size, only some representative publications are listed here. More comprehensive bibliographies may be found in Curry, Hindley and Seldin (1972), Hindley (1997), Anderson, Belnap and Dunn (1992), Terese (2003) as well as Hindley and Seldin (2008).
Anderson, A., N. Belnap, and J.M. Dunn, 1992. Entailment: The Logic of Relevance and Necessity (Volume II), Princeton: Princeton University Press.
Barendregt, H. P., 1981. The Lambda Calculus. Its Syntax and Semantics, (Studies in Logic and the Foundations of Mathematics: Volume 103), Amsterdam: North-Holland.
Barendregt, H., J. Endrullis, J. W. Klop and J. Waldmann, 2017. “Dance of the starlings,” in M. Fitting and B. Rayman (eds.), Raymond Smullyan on Self Reference, (Outstanding Contributions to Logic: Volume 14), Cham: Springer Nature, 67–111.
Bimbó, K., 2003. “The Church-Rosser property in dual combinatory logic,” Journal of Symbolic Logic, 68: 132–152.
–––, 2004. “Semantics for dual and symmetric combinatory calculi,” Journal of Philosophical Logic, 33: 125–153.
–––, 2005. “Types of I-free hereditary right maximal terms,” Journal of Philosophical Logic, 34: 607–620.
–––, 2007. “Relevance logics,” in D. Jacquette (ed.), Philosophy of Logic (Handbook of the Philosophy of Science: Volume 5), D. Gabbay, P. Thagard and J. Woods (eds.), Amsterdam: Elsevier/North-Holland, 2007, pp. 723–789.
–––, 2010. “Schönfinkel-type operators for classical logic,” Studia Logica, 95: 355–378.
–––, 2012. Combinatory Logic: Pure, Applied and Typed, Boca Raton, FL: CRC Press.
–––, 2014. Proof Theory: Sequent Calculi and Related Formalisms, Boca Raton, FL: CRC Press.
Bimbó, K., and J. M. Dunn, 2008. Generalized Galois Logics. Relational Semantics of Nonclassical Logical Calculi (CSLI Lecture Notes: Volume 188), Stanford, CA: CSLI Publications.
–––, 2012. “New consecution calculi for Rt→,” Notre Dame Journal of Formal Logic, 53: 491–509.
–––, 2013. “On the decidability of implicational ticket entailment,” Journal of Symbolic Logic, 78: 214–236
–––, 2014. “Extracting BB'IW inhabitants of simple types from proofs in the sequent calculus LTt→ for implicational ticket entailment,” Logica Universalis, 8(2): 141–164.
Broda, S., Damas, L., Finger, M. and P. S. Silve e Silva, 2004. “The decidability of a fragment of BB'IW-logic,” Theoretical Computer Science, 318: 373–408.
Bunder, M. W., 1992. “Combinatory logic and lambda calculus with classical types,” Logique et Analyse, 137–128: 69–79.
–––, 2000. “Expedited Broda–Damas bracket abstraction,” Journal of Symbolic Logic, 65: 1850–1857.
Cardone, F., and J. R. Hindley, 2006. “History of lambda-calculus and combinatory logic,” in D. M. Gabbay and J. Woods (eds.), Logic from Russell to Church (Handbook of the History of Logic: Volume 5), Amsterdam: Elsevier, 2006, 732–817.
Church, A., 1941. The Calculi of Lambda-conversion, 1st edition, Princeton, NJ: Princeton University Press.
Coppo, M., and M. Dezani-Ciancaglini, 1980. “An extension of the basic functionality theory for the λ-calculus,” Notre Dame Journal of Formal Logic, 21: 685–693.
Curry, H. B., 1963. Foundations of Mathematical Logic, 1st edition, New York: McGraw–Hill Book Company, Inc. (2nd edition, 1977, New York: Dover Publications, Inc.)
Curry, H. B., and R. Feys, 1958. Combinatory Logic (Studies in Logic and the Foundations of Mathematics: Volume I), 1st edition, Amsterdam: North-Holland.
Curry, H. B., J. R. Hindley, and J. P. Seldin, 1972. Combinatory Logic (Studies in Logic and the Foundations of Mathematics: Volume II), Amsterdam: North-Holland.
Dunn, J. M., 1991. “Gaggle theory: An abstraction of Galois connections and residuation with applications to negation, implication, and various logical operators,” in J. van Eijck (ed.), Logics in AI: European Workshop JELIA ’90 (Lecture Notes in Computer Science: Volume 478), Springer, Berlin, 1991, pp. 31–51.
Dunn, J. M., and R. K. Meyer, 1997. “Combinators and structurally free logic,” Logic Journal of IGPL, 5: 505–537.
Endrullis, J., J. W. Klop and A. Polonsky, 2016. “Reduction cycles in lambda calculus and combinatory logic,” in J. van Eijck, R. Iemhoff and J. J. Joosten (eds.), Liber Amicorum Alberti. A Tribute to Albert Visser (Tributes, Volume 30), London: College Publications, 111–124.
Fitch, F., 1942. “A basic logic,” Journal of Symbolic Logic, 7: 105–114.
–––, 1942. “An extension of basic logic,” Journal of Symbolic Logic, 13: 95–106.
Gierz, G., K. H. Hofmann, K. Keimel, J. D. Lawson, M. W. Mislove, and D. S. Scott, 2003. Continuous Lattices and Domains (Encyclopedia of Mathematics and its Applications: Volume 93), Cambridge: Cambridge University Press.
Gödel, K., 1931. “Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I,” in S. Feferman (ed.), Kurt Gödel: Collected Works (Volume I), New York and Oxford: Oxford University Press and Clarendon Press, 1986, pp. 144–195.
Hindley, J. R., 1997. Basic Simple Type Theory (Cambridge Tracts in Theoretical Computer Science: Volume 42), Cambridge: Cambridge University Press.
Hindley, J. R., and J. P. Seldin, 2008. λ-calculus and Combinators, an Introduction, Cambridge: Cambridge University Press.
Kleene, S. C., 1967. Mathematical Logic, New York: John Wiley & Sons, Inc; reprinted Mineola, NY: Dover, 2002.
Mackie, I., 2019. “Linear numeral systems,” Journal of Automated Reasoning, 63: 887–909.
Padovani, V., 2013. “Ticket Entailment is decidable,” Mathematical Structures in Computer Science, 23(3): 568–607.
Quine, W. V. O., 1960. “Variables explained away,” Proceedings of the American Philosophical Association, 104 (3): 343–347; reprinted in W.V.O. Quine, Selected Logical Papers, New York: Random House, 1966, 227–235.
–––, 1981. “Predicate functors revisited,” Journal of Symbolic Logic, 46: 649–652.
Révész, G. E., 1988. Lambda-calculus, Combinators and Functional Programming, Cambridge: Cambridge University Press.
Rezus, A., 1982. A Bibliography of Lambda-Calculi, Combinatory Logics and Related Topics, Amsterdam: Mathematisch Centrum.
Rosser, J. B., 1936. “A mathematical logic without variables,” Annals of Mathematics, 2: 127–150.
Schönfinkel, M., 1924. “On the building blocks of mathematical logic,” in J. van Heijenoort, (ed.), From Frege to Gödel. A Source Book in Mathematical Logic, Cambridge, MA: Harvard University Press, 1967, pp. 355–366.
Scott, D., 1970. Outline of a Mathematical Theory of Computation (Technical report), Oxford: Oxford University Computing Laboratory Programming Research Group.
–––, 1974. “The language Lambda, (abstract),” Journal of Symbolic Logic, 39: 425–426.
–––, 1976. “Data types as lattices,” SIAM Journal on Computing, 5: 522–587.
Seldin J. P., 2006. “The logic of Curry and Church,” in D. M. Gabbay and J. Woods (eds.), Logic from Russell to Church (Handbook of the History of Logic: Volume 5), Amsterdam: Elsevier, 2006, 819–873.
Smullyan, R. M., 1985. To Mock a Mockingbird. And other Logic Puzzles Including an Amazing Adventure in Combinatory Logic, New York: Alfred A. Knopf.
–––, 1994. Diagonalization and Self-reference, Oxford: Clarendon.
Updike, E. T., 2010. Paradise Regained: Fitch’s Program of Basic Logic, Ph.D. Thesis, University of California Irvine, Ann Arbor, MI: ProQuest (UMI).
–––, 2012. “Abstraction in Fitch’s basic logic,” History and Philosophy of Logic, 33: 215–243.
Tait, W., 1967. “Intensional interpretations of functionals of finite type I,” Journal of Symbolic Logic, 32: 198–212.
Terese (by Marc Bezem, Jan Willem Klop, Roel de Vrijer, Erik Barendsen, Inge Bethke, Jan Heering, Richard Kennaway, Paul Klint, Vincent van Oostrom, Femke van Raamsdonk, Fer-Jan de Vries and Hans Zantema), 2003. Term Rewriting Systems (Cambridge Tracts in Theoretical Computer Science: Volume 55), Cambridge: Cambridge University Press.
Academic Tools
Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO). | |
Enhanced bibliography for this entry at PhilPapers, with links to its database. |
Other Internet Resources
TLCA (Typed Lambda Calculi and Applications) open problem list
RTA (Rewriting Techniques and Applications) open problem list
Gentzen Working Group’s open problem list from the Utrecht ’93 meeting
Combinatory Logic page at Software and Tutorials for Instruction in Symbolic Logic in New Zealand.
Roger B. Jones’s λ-calculus website
Chris Rathman’s List of combinatory definitions
Related Entries
algebra | category theory | computability and complexity | Curry’s paradox | Gödel, Kurt | lambda calculus, the | logic, history of: intuitionistic logic | logic: intuitionistic | logic: linear | logic: relevance | logic: second-order and higher-order | logic: substructural | proof theory: development of | Quine, Willard Van Orman | reasoning: automated | recursive functions | Russell’s paradox | type theory | type theory: Church’s type theory
Acknowledgements
I am grateful to the referees of the first edition—both to the “internal referees” of this Encyclopedia and to Jonathan P. Seldin—for their helpful comments and suggestions, as well as certain corrections. Heeding the advice of the referees, I repeatedly tried to make the entry less technical and more readable.
最后更新于
