组合逻辑（三）

组合项WWW和WI(WI)或许是没有范式的最简单的例子。这两个项都诱导出一个无限归约序列，即一个无限的连续单步归约链。为了使示例更清晰，我们暂时假设W、I、C等不是由K和S定义的，而是原始常数。WWW中唯一索引的收缩返回相同的项，这表明唯一性并不意味着该项在nf中。 WI(WI) 中唯一索引的缩减得到 I(WI)(WI)，进一步化简为一开始的项。一个稍微复杂一点的例子是 Y(CKI)，它只具有无限化简序列。该项有一个化简序列（其中每个缩减的索引都以 Y 为首），其中包含无穷多个不同的项。也可以创建以 Y(CKI) 开头且具有各种循环的无限化简序列。总而言之，Church-Rosser 定理通常不能保证项 Q 的唯一性。但是，如果 M 具有范式，则它是唯一的。

Church-Rosser 定理通常表述如下。

Church-Rosser 定理 (II)。如果 N 和 P 相等，则存在一个项 Q，N 和 P 都可以化简为该项。

图 2

图 2。丘奇-罗瑟定理图解（二）

丘奇-罗瑟定理的第二种形式与第一种形式的区别在于其假设。从等式作为约简超集的定义来看，显然该定理的第一种形式蕴含于第二种形式。然而，尽管丘奇-罗瑟定理第二种表述的假设较弱，但这两个定理是等价的。等式是约简的传递对称闭包，这意味着如果两个项相等，则存在一条由约简和展开步骤组成的有限路径（分别分解为一步约简和一步展开）。然后，通过有限次应用第一丘奇-罗瑟定理（即通过对连接N和P的路径长度进行归纳），第一丘奇-罗瑟定理蕴含了第二种表述。

由于一步约简不具备钻石性质，因此对CL的丘奇-罗瑟定理的现代证明是间接进行的。当 xRy 和 xRz 蕴涵 yRv 和 zRv 时，二元关系 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)，菱形性质的失效就显而易见了。

一个合适的归约子关系是同时归约一组不重叠的redex，记为▹sr。“不重叠”是指两个redex之间不存在共同的子项。▹sr包含▹1，因为redex的一步归约可以看作是单例redex集的▹sr。▹sr显然包含在▹中（即包含在归约中）。这两个事实意味着，当考虑到自反传递闭包运算（记为∗）的强项性时，▹sr的自反传递闭包是归约。

(1)–(3)总结了上述关系之间的关键包含关系。

(1)

▹1⊆▹sr⇒▹

∗

1

⊆▹

∗

sr

(2)

▹sr⊆▹⇒▹

∗

sr

⊆▹∗

(3)

▹

∗

1

⊆▹∗ 且 ▹∗=▹。

我们需要的▹sr的核心性质正是以下定理的内容。

定理。（▹sr的菱形性质）如果 M▹srN 且 M▹srP，则存在一个项 Q 使得 N▹srQ 和 P▹srQ。

该定理的证明很容易对项 M 进行归纳。▹sr 的性质保证可以同时执行一个或多个单步归约，但这些归约不能相互干扰（或重叠）。

CL 的一致性由 Church-Rosser 定理以及（至少两个）不同范式的存在性得出。

定理。（一致性）CL 是一致的，即存在一些不能相互约简的项，因此它们不相等。

并非所有项都具有范式，但许多项确实具有范式。首先，例子包括 S 和 K。（变量，如果包含，其中有ℵ0个，都在nf中。）这些项都不包含redex，因此每个项只能归约到自身。根据Church-Rosser定理，排除了某些项M可以同时归约到x和S（使得S等于x）的情况。

然而，无限归约序列与nfs之间的相互作用值得更仔细地研究。项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 是一个（实际上也是唯一的）redex 的头，并且该项的头归约序列是无限的。由于 {S} 不包含任何具有抵消效果的组合子，因此，对于一个项，存在无限归约序列意味着该项没有 nf。在基 {S} 上存在更短的组合子，且不包含 nf，例如，S(SS)SSSSS 仅包含 8 个 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 在 nf 中，然而，在 nf 中并不是可定义的必要条件。使用 nf 中的定义项会更方便，因为应用不属于 nf 的组合子可以从将组合子化简为其标准形式开始。（此外，总是有无数个组合子可以化简为一个组合子。）然而，请注意，优先选择 nf 中的组合子并不意味着组合子不能由 nf 中的两个或多个项定义；下面我们给出 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的一些定义在约简方面具有略微不同的性质。但不动点组合子的重要性在于它确保所有函数都有不动点，并且所有递归方程都可以求解。

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 与图灵的不动点组合子类似。

不动点定理在一定程度上展现了 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) 中找到，由以下按其列出顺序应用的子句组成。

[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。此外，对于某个类型 X，Ix 的类型应为 X∘A 形式；那么 I 可以是 A→A 类型。在示例中，我们固定了 x 的类型，但 I 可以应用于任何项，因此更准确地说，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 与类型为

((B→B)→B)→(B→B)→B 的恒等组合子 I 不同。

这两种类型的类型有很多共同点，但也存在一些区别。具体来说，在 Church 类型的类型系统中，任何“自我应用”都无法被类型化，而有些术语在 Curry 类型的类型系统中可以被赋予类型。Curry 风格的类型系统在建立 CL 和 λ 演算的各种性质方面被证明非常有用。另一方面，Church 风格的类型系统更接近于某些函数式编程语言（无对象）中的类型。

在这两种类型系统中，类型和组合子之间不存在一一对应关系：并非所有组合子都能被赋予类型，并且某些蕴涵公式不能被赋予任何组合项。可以赋予类型的组合子被称为可类型化（typable），可以赋予组合子的类型被称为可归属（inhabited）。例如，M 没有（简单）类型，因为蕴涵公式永远不会与其自身的先行项相同。另一方面，皮尔士定律 ((A→B)→A)→A 不是类型赋值系统 TACL 中任何组合子的类型。尽管（或者实际上正是由于）蕴涵公式与组合项之间存在差异，但可以分配给某些组合项集的蕴涵公式类与一些重要逻辑的定理集相一致。

定理。A→B 是直觉主义蕴涵逻辑的一个定理，记为 IPC→ 或 J→，当且仅当对于某个 M，M:A→B 是 TACL 中的可证明类型赋值，其中项 M 由 S 和 K 构建，即 M 是基 {S,K} 上的组合子。

蕴涵定理中的组合子在演绎系统 TACL 中编码了该定理的证明。存在一种算法可以恢复构成组合子类型证明的公式，并且该算法可以生成最小且结构良好的证明。直觉逻辑的蕴涵定理（及其证明）与可典型闭合 λ 项（或组合子）之间的对应关系称为 Curry-Howard 同构。希尔伯特式公理系统中的证明通常概念较为宽松，但可以对其进行整理，得到遍历证明的概念。在遍历证明中，组合子的子项与遍历证明中的公式之间存在一一对应关系，应用与分离之间也存在一一对应关系（参见 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→B

B′ :(A→B)→(B→C)→A→C

C :(A→B→C)→B→A→C

W :(A→A→B)→A→B

S′ :(A→B)→(A→B→C)→A→C

I :A→A