组合逻辑（四）
组合基类 {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} 上有一个居住者，则它是可判定的。
该定理是相关蕴涵逻辑蕴涵片段可判定性的类型化等价物。R→ 的可判定性由 Saul A. Kripke 于 1959 年证明，同时证明了与之密切相关的 E→（蕴涵逻辑的蕴涵片段）的可判定性。
定理：若一个类型在基 {B,B′,I,W} 上有一个居住者，则它是可判定的。
该定理是票证蕴涵逻辑 T→ 蕴涵片段可判定性的类型化版本，该定理与 R→（真值常数为 t 的 R→）和 T
t
→
（真值常数为 t 的 T→）的可判定性一起由 Bimbó 和 Dunn (2012) 和 Bimbó 和 Dunn (2013) 证明。Padovani (2013) 提出了一个独立结果（仅适用于 T→），该结果扩展了 Broda 等人 (2004) 的成果。
T
t
→
和 R
t
→
的判定程序不使用 TACL 或公理演算，而是建立在序列演算（即结构连接词不假设具有结合性的序列演算）之上。结构规则与组合子之间存在关联的观点至少可以追溯到 Curry (1963)。为了加强这种联系，Dunn 和 Meyer（1997）引入了结构自由逻辑，其中组合子的引入规则取代了结构规则——因此得名这些逻辑。Bimbó 和 Dunn (2014) 提出了一种技术，可以从其在序贯演算中的标准证明中生成 T→ 定理的组合栖息子，该技术用于 T
t
→
的判定过程。序贯演算比自然演算或公理系统对证明的控制力更强。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 将不再具有类型性。在处处代换和完全不代换之间的一种折衷方案是修改分离规则，使其包含尽可能多的代换，以确保分离规则的适用性。这种规则（没有组合项或类型赋值）是由 Carew A. Meredith 在 20 世纪 50 年代发明的，通常被称为压缩分离规则。分离规则适用的关键在于找到小前提和大前提前件的共同代换实例。这一步称为合一。 （更正式地讲，设 s(A) 表示代换 s 对 A 的应用。那么，当存在一个 s 使得 s(A)=s(B) 时，将 A 从 B→C 中简洁地分离出来的结果是 s(C)，并且对于任何具有此性质的 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 的公式可以统一。这就是将合取 (∧) 和 top (⊤) 纳入为新类型构造函数的动机。
一个扩展的类型系统，通常被称为交集类型规则，归功于 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≤B
A≤B,B≤C ⇒A≤C
A≤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≤B
Δ⊢M:B
Δ⊢M:⊤
此类型赋值系统等价于λ演算的交集类型赋值系统，它能够更精确地刻画项类在归约序列终止方面的特征。
定理：
(1) 只要M可类型化，项M就规范化。
(2) 只要M可类型化且证明不包含⊤，项M就强规范化。
4. 模型
CL有各种类型的模型，本节将详细举例说明其中三个。对于2.1节中介绍的CL的不等式和方程系统，可以轻松构建代数模型（通常称为“项模型”）。项集构成一个代数，给定一个合适的等价关系（也为一致性），应用运算可以以标准方式提升到项的等价类。如此获得的代数的拟不等式刻画为这些逻辑的代数语义提供了基础。分离Lindenbaum代数并验证它不是平凡代数，构成了CL▹和CL=的一致性证明。
4.1 Scott的模型
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)，从而可以用自然数对 (n,m) 来刻画连续函数 f。
（有序）自然数对与自然数对之间的一一对应关系定义为
(n,m)=
[(n+m)⋅(n+m+1)]+2⋅m
2
构成（一元）函数的数对集合有时被称为该函数的图。连续函数 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 可由 I(MN)=fun(I(M))(I(N)) 扩展为复合项。（例如，设 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}。）) 该模型支持函数的内涵概念。
最早将类型无关的应用系统模型作为函数空间也是由 Scott 提出的，比图模型早几年，即 20 世纪 60 年代末。以下概述了该构造的一些关键要素。
在纯类型无关的 CL 中，形式为 MM 的表达式是一个合式项。此外，这种形式的项可以以多种方式代入可证明的方程和不等式中。例如，xx=xx 是一个公理，并且根据其中一条规则，y(xx)=y(xx) 也是可证明的。形式为 MM 的项的一个更有趣的例子可以在可证明的不等式 S(SKK)(SKK)x▹xx 中看到。
函数的集合论约简会得到一组对（通常为一组元组）。在集合论中（当然假设良基性），一个对（例如，{{a},{a,b}}）永远不会等于它的两个元素。因此，关于CL的数学模型的主要问题是如何处理自应用。
斯科特的原始模型是从完全格 (D,≤) 开始构建的。也就是说，(D,≤) 是一个偏序集，其中任意元素集都存在最大下界（最小确界）和最小上界（上确界）。从 (D,≤) 到完全格 (E,≤) 的函数 f，如果保持 D 上每个理想的上确界，则称其为连续的，其中理想是向上指向的向下闭合子集。
可以通过选择某些增集作为开集，在 D 上定义拓扑。更准确地说，如果 I 是理想，C 是锥，则 C 是开放的当且仅当 C∩I≠∅ 前提是 ⋁I∈C，即 I 的上确界是 C 的一个元素。（例如，主理想的补集是开放的。）f 在通常的拓扑意义上是连续的，即，当 D 和 E 连同它们的拓扑一起考虑时，开集的逆像也是开集。这促使我们早先将这些函数标记为连续函数。值得注意的是，所有连续函数都是单调的。
为了在 CL 中对函数进行建模，有趣的函数是那些在 D 上连续的函数。然而，这些函数本身不足以获得自应用的建模，因为它们都不以函数集作为其定义域——因为 D 不被假定为函数空间。解决方案始于定义一个函数空间的层次结构 D0、D1、D2、…，使得每个函数空间 Dn 都是一个完整的格，可以在其上定义连续函数（从而创建函数空间 Dn+1）。选择连续函数的重要性在于，新出现的函数空间与底层集合具有相同的基数，这使我们能够定义层次结构中相邻函数空间之间的嵌入。
