组合逻辑（二）

在发表第一篇关于基本逻辑的论文后的大约二十年里，Fitch 发表了一系列关于基本逻辑的论文，这些论文致力于探讨以下主题：(1) 递归函数的表示（即，论证了语法算术化的可能性）；(2) K′，K 的扩展，包含否定、全称量词和 （∗：算符的对偶）；(3) K 和 K′ 的一致性；(4) L，K′ 的扩展，包含蕴涵和必然算符；(5) 一些常数（例如 ∗ 和 ）以及：E 的可定义性。

K 中包含的组合子（因此，在其所有扩展中也包含）是 T、B 和 W。

ˊ

ε

和

ˊ

o

分别是 T 的三元版本和 B 的四元版本。罗素悖论涉及否定，但库里悖论（的任一变体）都是正的，因为它依赖于大卫·希尔伯特正蕴涵逻辑的一两个定理。这意味着，如果各种基本逻辑系统，尤其是K′和L，是一致的，那么它们要么不能包含完全抽象，要么蕴涵、蕴涵和恒等式的概念应该与它们通常的对应概念不同。事实上，K、K′ 和 L 不是外延系统。也就是说，即使两个表达式应用于同一个表达式总是相等，所应用的表达式也不一定相等。将基本逻辑转化为外延系统并非易事。Myhill 证明了 Fitch 的系统 JE′ 是不一致的，这导致了外延恒等式条件的更复杂的表述。

基本逻辑尚未成为广泛使用的描述形式系统的通用框架；然而，Updike (2010) 重新引起了人们对这种方法的兴趣，他试图将基本逻辑置于 20 世纪中叶基础工作的更广阔背景中。

奎因的消去策略

从 20 世纪 30 年代末开始，W. V. O. 奎因致力于研究一种从一阶逻辑中消去绑定变量的替代方法。可以合理地假设，Schönfinkel 的目标是在经典逻辑中找到一个算子，然后消除绑定变量（正如他在 Schönfinkel (1924) 中所声称的那样），而不是定义一个包罗万象的符号系统来描述所有数学。尽管如此，CL 很快就以一种更加自由的方式与经典逻辑融合，从而导致了一个不一致的系统。

Quine 找到了一种解决不一致问题的途径，即通过隐式地键入某种程度上类似于组合子的常量。他将这类常量称为谓词函子，并引入了几组，最后一组是在 Quine (1981) 中引入的。

FOL 最常见的表示形式是规定一个 n 位谓词后跟一个由 n 个项组成的序列（可能是，（用逗号标点并用括号括起来）是一个公式。（这与 Schönfinkel 的公式观点相反，并且与谓词作为 n 元关系的非正式和正式解释相一致。换句话说，FOL 不允许谓词或其解释的“柯里化”。）Quine 赞同项序列遵循谓词的观点。

谓词函子彼此之间不可应用——不像组合子那样。这是 Quine 反复强调的一点。原子谓词是一阶语言的谓词，而复杂谓词是通过将谓词函子（具有适当的元数）应用于谓词（可以是原子的或复杂的）获得的。

禁止自我应用以及使用“扁平”参数序列意味着需要无限多个谓词函子来确保从所有 FOL 公式中消除绑定变量。为了快速解释这个问题：一对任意远距离元素的排列无法保证其正确性，否则无法保证。正如组合子可以根据其效果分组一样，Quine 能够选择能够根据其效果自然分组的谓词函子。事实上，谓词函子的组类似于组合子的类，尽管 Quine 的标签通常很高级。为了给出这种替代方法的具体示例，我们概述了 Quine (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 元版本可以合并（通过忽略不受影响的参数），但 Inv 显然代表无穷多个谓词函子，因为 x1,…,xn 不能被忽略或省略。

值得注意的是，≀ 与 Schönfinkel 的 U 之间存在差异。不仅绑定变量的位置不同，而且≀ 还内置了 n-1 个变量的收缩（这些变量在左侧表达式中由 ∣− 和其他符号分隔）。

Quine 旨在用谓词函子语言实现一阶逻辑的新型代数化。虽然可以使用谓词函子消除绑定变量，但 Quine 从未定义过通常意义上的代数——例如类似于多元代数或圆柱代数的东西。谓词函子的设计使其适用性非常有限。这带来了一个不幸的副作用：它们似乎没什么意思，而且在预期语境之外用处不大。

2. 组合项及其主要性质

2.1 约简、相等及其形式化

乔治·康托尔和伯特兰·罗素在19世纪末20世纪初发现的悖论都涉及集合的自成员性。阿尔弗雷德·N·怀特黑德和伯特兰·罗素提出的分支类型理论，以及ZF（以恩斯特·策梅洛和亚伯拉罕·A·弗兰克尔命名的集合论形式化）都排除了自成员性。然而，人们似乎一直渴望创建一种允许自成员性或自应用性的理论。事实上，库里开发CL的动机之一就是构建一种包含各种合式表达式的形式语言，其中一些表达式——在某些解释下——可能变得毫无意义。 （这个想法可以与集合论的冯·诺依曼-伯奈斯-哥德尔形式化相比较，在该形式化中——无需基础公理——罗素类可以被证明不是集合，因此是一个真类。）

一些自然语言示例提供了一个便捷的例证，以阐明 (1) 与 (2) 之间的区别， (1) 是一个合式（但无意义）的表达式，而 (2) 是一个有意义（但形式错误）的句子。（当然， (2) 的意义应谨慎看待。实际上，库尔特·哥德尔在 1930 年证明了皮亚诺算术系统是不完备的。因此， (2) 可以通过句法和语义线索猜测为 (2′) 的扭曲版本，而皮亚诺算术在 1930 年已被哥德尔证明是不完备的。）

(1)

λx(x2+4x−6) 的导数试图表明函数是智能的。

（2）

1930年，哥德尔证明了皮亚诺算术的不完备性。在了解了这些非正式的动机之后，我们将转向 CL 本身，并更正式地介绍一些概念。

CL 中的对象称为项。[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

vs

(λy.y′)((λx.x2+4x−6)8)。

如果将词项视为结构化字符串（括号表示分组），则与长度为 n 的字符串相关联的不同词项的数量为 Catalan 数 Cn−1。对于非负整数 n（即 n∈N），

Cn=

1

n+1

(

2n

n

)。

前七个 Catalan 数分别为 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)。

所有项都被解释为函数，组合子也是函数。与一些易于描述和理解的数值函数和几何函数类似，常见的组合子也可以被描述为项的清晰变换。（无衬线字母表示组合子，▹1 表示一步化简。）

定义。（一些著名组合子的公理）

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 是复制器，因为在它们的应用结果中，其中一个参数（总是）出现两次。[10] C、T 和 V 是置换器，因为它们改变了部分参数的顺序。B 是一个结合器，因为 Bxyz 变成了一个项，其中先将 y 应用于 z，然后再将 x 应用于结果。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▹P

M▹P

M▹N

MP▹NP

M▹N

PM▹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 的术语是 redex，而前导组合子（分别为 S 和 K）是 redex 的头。如果项 Q 包含一个形式为 SMNP 的子项，则用 MP(NP) 替换该子项得到的 Q′ 是 Q 的一步约简。（对于索引 KMN 和 M 也类似。）也就是说，在两种情况下，Q▹Q′ 都是 Q。约简可以定义为一步约简的自反传递闭包。CL▹ 完全捕捉到了这个概念。演算 CL▹ 是完备的，因为如果 M▹N 符合我们刚才描述的意义，那么 CL▹ 就证明了 M▹N。（很容易看出，逆蕴涵也成立。）

约简的概念是一种比一步约简更弱的关系，因此使用更强的关系来区分项的子类很有用。当项不包含索引 KMN 和 M 时，它处于范式 (nf)。请注意，一步归约并不一定减少一个项所包含的重写操作总数，因此，并非所有项都可以通过有限多次一步归约变成nf中的项。事实上，有些项并不能归约成nf中的项。

归约可以说是表示函数的项之间的一种重要关系。程序执行和其他具体计算中的典型步骤是函数应用，而不是反方向的移动，后者被称为展开。然而，函数相等的概念在数学中为大家所熟悉，类似的概念也在CL中被引入。一步归约关系的传递性、自反性、对称性闭包称为（弱）相等。方程CL的形式化可以通过使用组合公理和刻画组合常数和应用运算的规则来扩展标准方程逻辑来获得。

CL (CL=) 的方程微积分。M=M KMN=M SMNP=MP(NP)

M=NN=P

M=P

M=N

N=M

M=N

MP=NP

M=N

PM=PN

第一个公理和前两个规则构成了等式逻辑。常数再次是组合子 S 和 K。注意，CL= 可以通过添加对称规则来定义为 CL▹ 的扩展，这与将归约中的等式定义描述为其传递对称闭包类似。我们选择用新的符号重复不等式公理和规则（并添加对称规则），以使这两个定义自洽且易于理解。= 的两个特征是一致的——就像 ▹ 的两个特征一样。

CL▹ 和 CL= 有一个共同的特征，这个特征可能是可取的，也可能不是——这取决于要捕捉对函数的何种理解。为了说明这个问题，我们考虑单元组合子 SKK 和 SK(KK)。很容易验证 SKKM▹M 和 SK(KK)M▹M。然而，无论是 SKK▹SK(KK) 还是 SK(KK)▹SKK，在 CL▹ 中都无法证明；更何况，这两个项的相等性在 CL= 中也无法证明。这意味着 CL▹ 和 CL= 形式化了函数的内涵概念，其中“内涵性”意味着，对于相同输入，输出相同的函数可能仍然具有可区分性。

人们可能遇到的典型内涵函数是算法。例如，我们可以想到各种计算 π 十进制展开式的规范，或者各种以相同方式运行的计算机程序。例如，编译器（针对同一种语言）可能因使用或不使用某些优化而有所不同，从而根据给定的代码片段生成具有相同输入输出行为但运行时间不同的程序。如果要识别从输入输出行为的角度无法区分的函数，即寻求对函数的外延理解，则必须通过以下规则扩展 CL▹ 和 CL=（其中符号 ‡ 分别替换为 ▹ 或 =）。

Mx‡Nx

M‡N

其中 x 在 MN 中不是自由的。

2.2 丘奇-罗瑟定理和一致性定理

上一节的演算 CL▹ 和 CL= 形式化地定义了约简和相等性。然而，▹ 和 = 具有一些进一步的性质，当它们被认为是函数时，这些性质非常重要。下一个定理是关于 CL 的最早和最著名的结果之一。

丘奇-罗瑟定理 (I)。如果 M 可以化简为 N 和 P，则存在一个项 Q，N 和 P 都可以化简为该项。

图 1

图 1. 丘奇-罗瑟定理图解 (I)

如果我们认为约简就像计算函数值一样，那么丘奇-罗瑟定理——在一级近似中——可以被认为是说，一系列带有一个项的计算的最终结果是唯一的——与步骤的顺序无关。但这略有夸大，因为唯一性意味着每一系列计算都会结束（或“循环”于一个项）。也就是说，如果存在唯一的最终项，那么只有有限多个不同的连续计算步骤是可能的。

或许，与初等算术运算进行粗略的类比可以解释这种情况。自然数的加法和乘法总是得出自然数。然而，如果包含除法，那么所有数值表达式的结果都为自然数就不再成立了，因为 7/5 是一个有理数，而不是自然数，而 n/0 是未定义的（即使 n 是实数）。也就是说，有些数值表达式的计算结果并非（自然）数。虽然与组合项的类比并不十分严谨，但仍然很有用。例如，n/0（假设函数λn.n/0的陪域被扩展，允许r为有理数）可以在计算机上通过一个循环（如果n≠0，则执行时永不终止）来实现，该循环将遍历有理数，试图找到一个满足r⋅0=n的r。