组合逻辑（六）

T_\rightarrow^\textbf{t} 和 R_\rightarrow^\textbf{t} 的决策过程不使用 \textrm{TA}_\textrm{CL} 或公理演算，而是建立在连续演算的基础上（即，连续演算，其中结构连接词不被假定为结合词）。结构规则和组合子之间存在密切关系的想法至少可以追溯到 Curry (1963)。为了加强联系，Dunn 和 Meyer (1997) 引入了结构自由逻辑，其中组合器的引入规则取代了结构规则——因此这些逻辑的标签。 Bimbó 和 Dunn (2014) 引入了一种技术，可以根据后续微积分中的标准证明生成 T_\rightarrow 定理的组合居民，该技术用于 T_\rightarrow^\textbf{t} 的决策过程。与自然演绎或公理系统相比，顺序演算可以更好地控制证明。 Bimbó 和 Dunn (2014) 的组合提取过程在组合子和基于连续微积分证明的类型之间产生了有效的联系，这消除了 \textrm{TA}_\textrm{CL} 和公理系统的明显优势。

替换规则通过称为分离的规则模式和基本组合器的公理模式内置到 \textrm{TA}_\textrm{CL} 的公式中。显然，存在最简单复杂度的公式是 \textsf{S} 和 \textsf{K} 类型，因此所有其他类型的 \textsf{S} 和 \textsf{K} 都是它们的替换实例。具有此属性的公式称为组合器的主要类型。显然，一个具有主类型的组合器有可数多个主类型，它们都是彼此的替换实例；因此，讨论组合器的主要类型模式是合理的。然而，复杂组合子的主要类型的存在性并不明显。

如果术语 M 是可键入的，则 M 具有主体类型和主体类型模式。

现在，主体类型和主体类型模式似乎在任何地方都可以互换。因此，我们可以采取稍微不同的方法并定义 \textrm{TA}_\textrm{CL} 以包含公理和分离规则模式以及替换规则。此版本的 \textrm{TA}_\textrm{CL} 将采用以下形式。

\Delta\vdash\textsf{S}\冒号(p \rightarrow q\rightarrow s)\rightarrow(p\rightarrow q)\rightarrow p\rightarrow s \Delta\vdash\textsf{K}\冒号q\rightarrow s\ rightarrow q \frac{\Delta\vdash M\colon A\rightarrow B\qquad \Theta\vdash N\colon A} {\Delta,\Theta\vdash MN\colon B} \frac{\Delta\vdash M\colon A} {\Delta[P/B]\vdash M\colon A[P/B]}

其中 P 范围涵盖命题变量。 （替换符号以明显的方式扩展到类型赋值集。）显然，这两个演绎系统是等效的。

如果完全放弃替换，那么分离的适用性将变得极其有限，例如， \textsf{SK} 将不再是可输入的。到处都有替换和根本没有替换之间的折衷是修改分离规则，以便包括尽可能多的替换，以确保分离规则的适用性。这样的规则（没有组合术语或类型分配）是由 Carew A. Meredith 在 20 世纪 50 年代发明的，通常称为压缩分离。分离适用的关键是找到小前提和大前提的先行词的共同替换实例。这一步称为统一。 （更正式一点，让 s(A) 表示将 s 替换到 A 上。然后，当存在 s 使得 s 时，A 与 B\rightarrow C 的压缩分离的结果是 s(C) (A)= s(B)，对于任何具有此性质的 s_1，都存在一个 s_2，使得 s_1 是 s 和 s_2 的组合。）

请注意，总是可以选择一对公式的替换实例，以便其命题变量的集合不相交，因为公式是有限对象。两个公式 A 和 B（不共享命题变量）的最常见实例是 C，其中 C 是 A 和 B 的替换实例，并且仅当需要识别命题变量时，才通过替换来识别命题变量。获得一个公式，它是 A 和 B 的替换实例。统一定理（专门用于简单类型）意味着，如果两个公式 A 和 B 有一个公共实例，则存在一个公式 C，使得 A 和 B 的所有公共实例B 是 C 的替换实例。显然，一对公式要么根本没有公共实例，要么具有 \aleph_0 许多最通用的公共实例。

一对没有公共实例的公式的一个著名例子是 A\rightarrow A 和 A\rightarrow A\rightarrow B。实例 p \rightarrow p 和 q\rightarrow q\rightarrow r 不共享命题变量，但是 q 也不共享命题变量。 \rightarrow q 或 (q\rightarrow r)\rightarrow q\rightarrow r 与第二个公式的形状匹配。换句话说，q 和 q\rightarrow r 必须统一，但无论用什么公式代替 q，它们都不能统一。这样做的直接后果是 \textsf{WI} 不可输入。

另一方面，

(r\右箭头 r)\右箭头 r\右箭头 r

和

((s\右箭头 s)\右箭头 s\右箭头 s)\右箭头 (s \右箭头 s)\右箭头 s\右箭头 s

是 p\rightarrow p 和 q\rightarrow q 的替换实例。此外，所有简单类型都是命题变量的替换实例，因此 \textsf{II} 可以被指定为类型 r\rightarrow r 和类型 (s\rightarrow s)\rightarrow s\rightarrow s——当然，后者恰好是前者的实例，因为 A\rightarrow A 是 \textsf{II} 的主要类型模式。如果我们将压缩分离应用于 p\rightarrow p 和 q\rightarrow q，那么我们得到 q\rightarrow q （通过替换 [p/q\rightarrow q] 和 [q/q]），因此压缩分离产生本金\textsf{II} 的类型。顺便说一句， \textsf{II} 和 \textsf{I} 提供了一个很好的例子来说明不同的术语可能具有相同的主体类型模式。

压缩分离已被广泛用于完善各种蕴涵逻辑的公理化，特别是在寻找更短和更少的公理时。一些逻辑可以使用公理（而不是公理模式）以及压缩分离规则来表述，而不会丢失定理。到目前为止我们提到的所有逻辑（J_{\rightarrow}、R_{\rightarrow}、T_{\rightarrow} 和 E_{\rightarrow}）都是 \mathbf{D} 完备的，也就是说，它们都可以被公理化通过公理和浓缩超然规则。也就是说，经典逻辑和直觉逻辑的蕴涵片段，以及关联逻辑R、E和T的蕴涵片段都是\mathbf{D}完备的。 （有关更多技术细节，请参见 Bimbó (2​​007)。）

简单类型系统已向各个方向扩展。逻辑常常包含超出暗示的连接词。这是对类型分配系统的自然修改，通过包含更多类型构造函数来扩展类型集。连接和融合作为类型构造函数是最容易解释或激发的，然而，析取和向后蕴涵也被引入到类型中。类型很有用，因为它们使我们能够从术语的归约行为的角度来掌握术语的类别。

泰特定理。如果组合项 M 是可类型化的（具有简单类型），则 M 强归一化，即 M 的所有约简序列都是有限的（即终止）。

显然，这种说法的反面是不正确的。例如，\textsf{WI} 强烈规范化但不可类型化，因为收缩的先行词不能与任何自我暗示的实例统一。扩展可打字术语集的目的导致了将 \land 引入类型中。

3.2 交叉口类型

看待输入 \textsf{WI} 问题的另一种方式是说 \textsf{W} 应该具有类似于公式 (A\rightarrow (A\rightarrow B))\rightarrow A\rightarrow B 的类型，但其中代替先行词中的两个公式 A 和 A\rightarrow B 的公式可以统一。这是包含连词 (\land) 和顶部 (\top) 作为新类型构造函数的动机。

扩展类型系统，通常称为交叉类型规则，是由 Mario Coppo 和 Mariangiola Dezani-Ciancaglini 提出的。交集类型集（用 wff 表示）定义如下。

p\in\textrm{wff} 如果 p 是命题变量；

\top\in\textrm{wff}，其中 \top 是一个常数命题；

A, B\in\textrm{wff} 意味着 (A\rightarrow B),(A\land B)\in \textrm{wff}。

当然，如果 TA_\textrm{CL} 增加了一组扩展的类型，则先前分配的类型的新实例将变得可用。然而，具有新类型构造函数 \land 和 \top 的类型的要点是，类型集具有比由替换规则和肯定前件规则确定的类型之间的关系更丰富的结构。

交集类型的结构由 B 的合取蕴涵片段（基本关联逻辑）描述。在下面的逻辑演示中，\le 是公式的主要连接词（蕴涵），\Rightarrow 分隔推理规则的前提和结论。

\begin{align*} A\le A\qquad A\le\,&\,\top\qquad\top\le\top\to\top\\ A\le A\land A\qquad A\land B&\ ;\le A\qquad A\land B\le B\\ A\le B,\,B\le C&\;\Rightarrow A\le C \\ A\le B,\,C\le D\Rightarrow&\ ; A\land C\le B\land D \\ (A\rightarrow B)\land(A\rightarrow C)\le&\;(A\rightarrow (B\land C)) \\ A\le B,\, C\le D\右箭头&\; B\右箭头 C\le A \右箭头 D \end{对齐*}

组合符 \textsf{S}、\textsf{K} 和 \textsf{I} 的公理模式如下。请注意，\textsf{S} 的公理不仅仅是先前 \textsf{S} 公理的替换实例（包括新的连接词）。

\Delta\vdash\textsf{S}\colon(A\rightarrow B\rightarrow C)\rightarrow(D\rightarrow B)\rightarrow(A\land D)\rightarrow C \Delta\vdash \textsf{K}\colon A\右箭头 B\右箭头 A \qquad \Delta\vdash \textsf{I}\冒号 A\右箭头 A

添加了四个新规则，并且有一个 \top 公理。

\frac{\Delta\vdash M\冒号 A\quad\Delta\vdash M\冒号 B} {\Delta\vdash M\冒号 A\land B} \quad \frac{\Delta\vdash M\冒号 A\land B} {\Delta\vdash M\冒号 A} \quad \frac{\Delta\vdash M\冒号 A\land B} {\Delta\vdash M\冒号 B} \frac{\Delta\vdash M\冒号 A \qquad A\le B} {\Delta\vdash M\colon B} \quad \Delta\vdash M\colon\top

该类型分配系统等价于 lambda 演算的交集类型分配系统，并且它允许更精确地表征关于归约序列终止的项类。

定理。

(1) 只要 M 是可输入的，术语 M 就会标准化。

(2) 只要​​ M 是可输入的并且证明不包含 \top，术语 M 就会强规范化。

4. 型号

CL 有多种模型，本节将详细介绍其中三种模型。对于 2.1 节中介绍的 CL 不等式系统和方程系统，可以毫无困难地构建代数模型（通常称为“项模型”）。术语集形成一个代数，并且给定适当的等价关系（即同余），应用操作可以以标准方式提升到术语的等价类。如此获得的代数的拟不等式表征为这些逻辑的代数语义提供了基础。分离 Lindenbaum 代数并验证它不是平凡代数构成了 \text{CL}_\triangleright 和 \text{CL}_= 的一致性证明。

4.1 斯科特的模型

Dana Scott 为 lambda 演算定义了 P\omega 和 D_\infty。我们先概述一下P\omega——所谓的图模型，比较容易理解。

自然数具有非常丰富的结构。 P\omega 是自然数集的幂集，它是具有相同标签的模型的核心。每个自然数在基数 2 中都有唯一的表示形式。（例如，7_{10} 是 111，即 7=1\cdot2^2+1\cdot2^1+1\cdot 2^0=4+2+1 .) 每个二进制表示形式为

b_m\cdot2^m+b_{m-1} \cdot2^{m-1}+\cdots+b_1\cdot 2^1+b_0\cdot2^0 ,

其中每个b是0或1。那么每个二进制数可以被视为自然数的有限子集的特征函数。 （左边有无穷多个零，如 \ldots000111 所示，被省略。）对于自然数 n，e_n 表示相应的有限自然数集。 （例如，e_7=\{0,1,2\}。）

P\omega 上的正拓扑包含有限生成的开集。令 E 表示 Ω 的有限子集。 X\subseteq P\omega 是开放的，当且仅当 X 是由 E 的子集生成的圆锥体（相对于 \subseteq）。给定正拓扑，函数 f\colon P\omega\rightarrow P\omega 结果是连续的（在通常的拓扑意义上）iff f(x)=\cup\{f(e_n)\colon e_n\subseteq x\}，其中 e_n\in E。这意味着 m\in f(x) iff \存在 e_n \subseteq x.\, m\in f(e_n)，这导致用自然数对 (n,m) 来表征连续函数 f。

（有序）自然数对与自然数之间的一一对应关系定义为

(n,m) = \frac{[(n+m)\cdot(n+m+1)]+2\cdot m} {2}

构成（一元）函数的对的集合有时称为函数的图。连续函数 f\colon P\omega\rightarrow P\omega 的图由 \textrm{graph}(f)=\{(n,m)\colon m\in f(e_n)\} 定义。为了能够对无类型应用程序（包括自应用程序）进行建模，Ω 的子集也应被视为函数。对于 x, y\subseteq\omega，y 确定的函数定义为 \textrm{fun}(y)(x)=\{m\colon \exists e_n\subseteq x.\,(n,m)\in y\}。对于连续函数 f，\textrm{fun}(\textrm{graph}(f))=f 成立。

CL 的图模型将项映射到 omega 的子集。首先，组合器有具体的集合作为它们的解释。举个简单的例子，\textsf{I}= \{(n,m)\colon m\in e_n\}。当然，每一对都对应于 omega 的一个元素，因此，我们得到了一组自然数。特别是，一些元素是\{1,6,7,11,15,23,29,30,\ldots\}。

如果组合器（以及变量）被解释为 omega 的子集，则函数应用程序应采用第一组（视为 P\omega\rightarrow P\omega 类型的函数）并将其应用于第二组。 \textrm{fun}(y) 是一个由 y \subseteq\omega 确定的合适函数。一般来说，如果 M 和 N 是 CL 项，并且 I 是将原子项解释为 P\omega，则 I 通过 I(MN)=\textrm{fun}(I(M))( 扩展到复合项（例如，令I(x)为e_9=\{0,3\}。I(\textsf{I}x)=\textrm{fun}(I(\textsf{I}))(I (x))=\{m\colon \exists e_n\subseteq I(x).\,(n, m)\in I(\textsf{I})\} 我们知道 I (\textsf{I})。 ) 和 I(x) 是；因此，我们进一步得到 I(\textsf{I}x)= \{m\colon\exists e_n\subseteq e_9.\,m\in e_n\} 当然，\{ 0,3\}\subseteq \{0,3\}，因此我们有 I(\textsf{I}x)=\{0,3\}。）该模型支持函数的内涵概念。

在60年代后期，在图模型之前的几年，Scott也给了Scott的最早模型作为功能空间。以下是建筑的一些关键要素的概述。

在纯字体CL中，MM形式的表达是一个形成良好的项。此外，此形式的术语可以以多种方式进入可证明的方程式和不等式。例如，xx = xx是一个公理，通过其中之一，y（xx）= y（xx）也是可证明的。在可证明的不音机\ textsf {s}（\ textsf {skk}）（\ textsf {skk}）x \ triangleright xx中可以看到更有趣的术语。

函数的设定理论降低产生一组对（通常是一组元组）。在集合理论（当然，假设有充分的基础）中（例如，\ {\ {a \}，\ {a，b \} \}）绝不与其两个元素之一相同。因此，有关CL数学模型的主要问题是如何处理自我应用。

Scott的原始型号是从完整的晶格（D，\ le）开始的。也就是说，（d，\ le）是一个部分有序的集合，其中最大的下限（INFIMA）和最小的上限（suprema）存在于任意元素集。从（d，\ le）到一个完整晶格（E，\ le）的功能f被认为是连续的，当它保留了D上的每个理想的上限时，理想是一个理想的向上定向向下的闭合子集。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。