组合逻辑（五）

所有函数空间 Dn 的层次结构可以累积在一起。模型论中的一个标准构造是形成结构的不相交并集。 （通过索引结构的载体集，始终可以保证不相交性。）斯科特将 D∞ 定义为函数空间 Dn 的不相交并集，对于所有 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 and Meyer (1997)）。CL 和 λ 演算与直觉逻辑、关联逻辑和其他非经典逻辑有着内在联系。特别是 CL▹ 和 CL= 演算本身就是非经典逻辑。自 20 世纪 60 年代初以来，内涵连接词由一系列情境上的关系建模的集合论语义一直是非经典逻辑的首选解释。这类语义有时被称为“克里普克语义”（因为克里普克于 1959 年为某些正态模态逻辑引入了可能世界语义）或“群语义”。 （源自 Dunn (1991) 提出的“广义伽罗瓦逻辑”缩写“ggl”的发音）。

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有效，如果v(M)⊆v(N)在CL▹框架的所有赋值下成立。 （也就是说，每当 v 在变量集上变化时，两个项的解释之间的关系不变。）

非正式地，底层集合 W 是情境的集合，R 是连接情境的可及性关系。所有项都被解释为情境集，函数应用是从 R 派生出的存在性图像运算。与之前的模型不同，一个项应用于另一个项的结果不是由解释这两个项的对象本身决定的——而是应用运算是由 R 定义的。

该语义推广了正则模态逻辑的可能世界语义。因此，需要注意的是，这些情境并非最大一致性理论，而是具有以下性质的理论：对于任何一对公式，它们都包含一个蕴含这两个公式的公式。等价地，这些情境可以被视为 CL▹ 的 Lindenbaum 代数上的对偶理想。这些情境通常是一致的，因为它们除了一种情况外，并不包含所有项。 （否定一致性的概念，当然，不能为 CL▹ 或 CL= 定义。

关系语义可以类似地为 CL= 定义。这样，可靠性和完备性（即以下定理）就成立了。

定理：

(1) 不等式 M▹N 在 CL▹ 中可证明，当且仅当 v(M)⊆v(N) 在 CL▹ 的任何模型中成立。

(2) 等式 M=N 在 CL= 中可证明，当且仅当 v(M)=v(N) 在 CL= 的任何模型中成立。

包含对偶和对称组合子的 CL 系统的关系语义和操作语义可参见 Bimbó (2​​004)。

5. 可计算函数和算术

CL 的一个显著特点是，尽管看似简单，但它却是一种强大的形式主义。当然，如果不发现组合项之间的某些关系，或者不说明可计算函数是可定义的，就无法体会CL的强大之处。

数学形式化的一个重要起点是算术的形式化，这首先由戴德金-皮亚诺公理化实现。在CL中，有多种方法可以形式化算术；本节将介绍两种数的表示形式以及一些基于它们的函数。

数可以被认为是某种对象（或抽象对象）。（此处的数指的是自然数，即0和正整数。）例如，数可以通过它们作为集合所具有的结构来表征。这种结构支持诸如0≠1之类的属性，以及n与m之和等于m与n之和。自然数的另一个众所周知的属性是，例如，存在无穷多个素数。

在 CL 中，数字可以用项来表示，其中一种方法是选择 KI、I、SBI、SB(SBI)……来表示 0、1、2、3 等。表示算术运算的项各不相同，取决于哪些项代表数字。需要注意的是，与戴德金-皮亚诺的算术形式化不同，CL 没有做出类似于单个常量和函数符号之间区别的句法区分——在 CL 中，唯一的对象是项。上面的项列表已经显示了后继函数，即 SB。（SB(KI) 强等于 I，即 1 是 0 的后继。）

加法是项 BS(BB)，乘法是项 B。基于加法的乘法的通常递归定义可能表明加法应该比乘法更简单。然而，在 CL 中，数字本身就是函数，因此它们具有一些属性，使得 B——一个看起来更简单的项——可以被选为通常被认为比加法更复杂的函数。（加法运算可以用原始递归来定义，这将产生一个更复杂的项。）作为一个经典的例子，我们可以考虑项 BII，它强等于 I，即 1×1=1——正如预期的那样。我们在此不再赘述这种数值表示。我们只需指出，这些数的形状与λ演算中的丘奇数密切相关，每个丘奇数都是一个二元函数（而这里每个数都是一个一元函数）。

在CL中表示数的另一种方法是从不同的数项开始。之前，I代表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。

某些计算模型（例如寄存器机）和某些编程语言包含对零的测试作为基本构造。找到函数 Z 的 CL 项很有用，使得当 n 为零时，Znxy 归约成 x，而当 n 为正时，Znxy 归约成 y。Znxy 可以被认为是条件指令“如果 n=0 则 x 否则 y”，其中 x 和 y 本身是函数。（当然，在伪代码中应该假设 n 是整数类型并且不能取负值，这可以通过声明变量并附加条件语句来保证。）以下定义适用于从零分支的情况。

Z=TK

TKnxy=nKxy，如果 n 为零，即 n=1，则进一步归约得到 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(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，它们的行为与目标函数在数字上的行为相同。也就是说，定义算术函数的一个同样好的方法是简单地列出一些项，然后证明它们的行为符合预期。然而，一旦证明了基本的原始递归函数以及递归和最小化可以在 CL 中模拟，我们不仅得到了一个以组合子形式存在的算术函数集合，而且还证明了组合逻辑具有足够的表达能力来形式化所有部分递归函数。事实上，此类证明的其余步骤可以在 CL 中执行，尽管细节超出了本文的范围。

5.1 哥德尔句子

上图简述中的缩写和穿插的解释可能掩盖了这样一个事实：算术已经以一种由五个符号（不计算并列符号时）组成的语言形式化：S、K、= 加上两个分隔符 ( 和 )。有限的（或许，符号数量（数量少得惊人）以及递归函数的可用性，使人想到可以尝试对 CL 的语法进行算术化。

哥德尔通过将数字分配给符号、公式和公式序列（后来被称为“哥德尔数”），实现了形式语言的编码。具体来说，哥德尔将奇数分配给符号，将素数幂的乘积（数字对应于指数中的符号）分配给符号序列。然而，无需过分强调素数的存在和性质，就可以对 CL 语言进行算术化。（例如，参见 Raymond M. Smullyan 的著作：Smullyan (1985) 和 Smullyan (1994)。）这五个符号的前五个正整数作为它们的哥德尔数。将符号对应数字连接起来得到的十进制数赋给一个字符串。

以下概述了适用于 CL 的哥德尔不完备定理的类似物。可以定义一个组合子，如果将此组合子应用于数字 n，则整个项简化为数字 m，该数字表示数字 n 的哥德尔数。更正式地说，存在一个组合子 δ，使得 δn=G(n)（其中 G(n) 表示表达式 n 的哥德尔数）。此外，还有一个组合项，当应用于数字 n 时，它返回数字本身，后跟 G(n)。对于任何项 A，存在一个项 B，使得方程 A(δB)=B 为真。这个陈述（或其针对特定形式系统的具体变体）通常称为第二不动点定理。递归数集的可计算特征函数可以用组合子表示，其中K表示真，KI表示假。此类函数的补函数也是可计算的。最后，可以证明不存在能够表示所有真方程集的组合子。换句话说，任何组合子要么表示一组不包含某些真方程的方程，要么表示一组包含所有真方程但也包含某些假方程的方程。

Alonzo Church 依据哥德尔不完备定理证明了经典一阶逻辑的不可判定性。Dana Scott 证明，如果 A 是λ项的非空真子集，并且在等式下封闭，则 A 不是递归的。对于CL，类似的断言（由CL的哥德尔语句的存在得出）是，如果两个CL项相等，则它是不可判定的。