证明与类型

前言

这本小书来源于1986至1987年秋季学期于Université Paris VII开设的一门关于类型$\lambda$演算的短期研究生课程. 它并不意图是百科全书式的, 例如Church-Rosser定理就没有证明, 而且主题的选取是相当随意的.

关于逻辑的基本常识是必要的, 然而我们也并不会陷入乏味的细节之中.

第1章 涵义, 指称和语义

理论计算尚非科学. 许多基本概念亟待澄清, 并且当前该领域的研究遵循一种"婚礼蛋糕"范式: 例如, 语言设计让人想到Ptolemy天文学——不断需要更加深入的修正. 然而, 也存在一些有限的主题, 例如复杂度理论和指称语义学, 它们相当远离这种批判.

在这样的情况下, 方法论式的评论极其重要, 因为我们不得不将方法论视为战略而将具体的结果视为具有战术性质.

我们尤其感兴趣的东西可在1900年代的逻辑漩涡的源头找到, 由Frege, Löwenheim, Gödel等名字刻画. 不熟悉逻辑学史的读者应该参考[4].

第1.1节 逻辑中的涵义和指称

让我们从一个例子开始. 存在一个乘法的标准过程, 它由输入$27$和$37$产生结果$999$. 对于这个事实我们可以言称什么?

最初的尝试是言称我们拥有了一个等式$$27\times 37=999$$这个等式在数学主流中以言称两边指称相同的整数且$\times$是Cantor的图的意义下的一个函数而获得了含义. (译注: 这里"整数"的原文是"integer", 又有原注, 全文的integer将表示natural number: $0,1,2,\dots$)

这是指称性的方面, 无疑是正确的, 然而它忽略了基本的点.

存在一个有限的计算过程表明这两个指称是相等的. 言称$27\times 37$等于$999$是一种滥用 (这并非什么廉价的哲学——而是一个具体的问题), 因为如果我们所拥有的这两个东西真是相同的, 那么我们就不会感到陈述它们的相等性的需要了. 具体地说, 我们在问一个问题, $27\times 37$, 然后得到了一个答案, $999$. 这两个表达式具有不同的涵义, 而我们必须做些什么 (编制证明或者进行计算, 或是至少查询百科全书) 来表明这两个涵义具有相同的指称.

关于$\times$, 将其称为一个(作为图的)函数是不正确的, 因为加载了乘法程序的机器无法容纳下一个无限的图. (译注: 这句话是说实无限是不可能容纳于一个经典计算机器之中的, 当然潜无限的确是可以的.) 因此, 我们不得不总结道, 我们面对的是与这个涵义之问相关的一种有限的动力学.

尽管指称在很早的阶段就被建模, 涵义则被推向了主观主义, 导致当前的数学对于涵义的处理或多或少沦为了句法操作. 这在我们所要讨论的主题的本质之下并非先验, 而我们可以期待在接下来的几十年里找到一种对于计算的处理, 它结合了指称语义学 (数学的清晰性) 和句法 (有限的动力学) 的优点. 本书显然坐落于传统之上, 这种传统基于不幸的当前状况: 在无限的静态的指称与有限的动态的涵义的对立之中, 指称性的一方要远比另一方先进.

于是乎, 逻辑中由Frege指出的最根本的一个区分是: 给定一个句子$A$, 存在两种看待它的方式:

• 作为指令的序列, 确定了其涵义, 例如$A\vee B$的意思是"$A$或$B$", 等等.
• 作为由这些操作找到的理想结果: 此即其指称.

第2章 自然演绎

正如我们之前所言, 句法性的观点展现了逻辑学的某种深远的对称. Gentzen的相继式演算以特别令人满意的方式完成了这种观点. 不幸的是, 其计算上的意义在某种程度上被其句法上的复杂性所掩盖, 尽管这种复杂与本质无关, 但是从来没有真正被克服. 这就是为什么我们在处理相继式演算之前要先呈现Prawitz的自然演绎.

自然演绎在某种意义上是有点悖论性的系统. 其局限于直觉主义的情形 (在古典情形下没有什么良好的性质), 但是它也只是对于语言的$(\wedge ,\Rightarrow ,\forall )$部分令人满意而已: 我们将对于$\vee$和$\exists$的考虑推迟到第10章. 尽管如此, 析取和存在是两种最典型的直觉主义的联结词!

自然演绎的基本想法是一种不对称: 一个证明大致上是一个树状的结构, 其有一个或多个假设 (也可能没有), 但是只有一个结论. 这种演算的深刻对称在于相互精准匹配的引入和消去规则. 我们应该顺便观察到这样的事实, 对于这样一种树状结构, 我们总是可以唯一地确定哪一条规则是最后被使用的. 如果有多个结论的话, 那是无法做到的.

第2.1节 演算

我们将使用记号$$\begin{array}{c}⋮\\ A\end{array}$$来指对于$A$的一个演绎(deduction), 即停止于$A$. 这个演绎会被写成一个有限的树的形式, 并且树的叶子会被标记以句子. [译注: 这个指的不是带标签的树 (labelled tree).] 对于这些句子, 存在两种可能的状态, 死或生. [译注: 更准确地说, 是对于这些叶子.]

在通常状态下, 一个句子是活着的, 也就是说其在证明中还处于活跃的地位: 我们称其是一个假设(hypothesis). 典型的情况由自然演绎的第一条规则刻画, 其允许我们构造一个仅包含一个句子的演绎:$$A$$这里的$A$既是叶子也是根; 从逻辑上说, 我们推出了$A$, 但这只是因为$A$是被假定成立的!

现在位于叶子位置的句子是可以死去的, 当其不再于证明中活跃时. 死去的句子可以通过杀死活着的句子得到. 最典型的例子是$\Rightarrow$的引入规则:$$\frac{\begin{array}{c}[A]\\ ⋮\\ B\end{array}}{A\Rightarrow B}\Rightarrow \mathcal{I}$$以上的演绎必须按照如下方式理解: 我们从$B$的一个演绎开始, 在这个$B$的演绎中, 我们选取了特定数目的$A$的出现作为假设 (这个数字可以是任意的: $0,1,250,\dots$), 然后我们构造了一个新的演绎, 其结论是$A\Rightarrow B$, 但是其中的这些选定的$A$的出现都会被discharged, 即被杀死. 可能还存在其他$A$的出现我们选择不去discharge.

这条规则很好地刻画了树状的记号的样貌: 知道何时一个假设被discharged是重要的, 因而有必要记录这种信息. 但是如果在以上的例子中这样做, 这意味着我们需要将被叉掉的$A$和$\Rightarrow \mathcal{I}$规则那行连起来; 但是连起来之后这个东西就不再是之前我们所考虑的真正的树结构了!

第2.1.1小节 规则

• 假设: $A$
• 引入:$$\frac{\begin{array}{c}⋮\\ A\end{array}\begin{array}{c}⋮\\ B\end{array}}{A\wedge B}\wedge \mathcal{I}\frac{\begin{array}{c}[A]\\ ⋮\\ B\end{array}}{A\Rightarrow B}\Rightarrow \mathcal{I}\frac{\begin{array}{c}⋮\\ A\end{array}}{\forall \xi .A}\forall \mathcal{I}$$
• 消去:$$\frac{\begin{array}{c}⋮\\ A\wedge B\end{array}}{A}\wedge 1\mathcal{E}\frac{\begin{array}{c}⋮\\ A\wedge B\end{array}}{B}\wedge 2\mathcal{E}\frac{\begin{array}{c}⋮\\ A\end{array}\begin{array}{c}⋮\\ A\Rightarrow B\end{array}}{B}\Rightarrow \mathcal{E}\frac{\forall \xi .A}{A[a/\xi ]}\forall \mathcal{E}$$在传统上$\Rightarrow \mathcal{E}$被称为modus ponens.

一些注记:
所有的规则, 除了$\Rightarrow \mathcal{I}$, 都保持the stock of hypotheses: 例如, 以上以$\Rightarrow \mathcal{E}$作结的演绎, 其假设是两个立即子演绎的假设.
出于众所周知的逻辑原因, 有必要将$\forall \mathcal{I}$限制于变量$\xi$不能在任何假设中自由出现的情形 (但是, 从另一方面说, 其可以在死去的叶子中自由出现).
这个系统的基础对称在于引入/消去对称, 其代替了不能在这种上下文中被实现的假设/结论对称.

原注: 变量$\xi$属于对象语言 (其可能代表一个数字, 一个数据记录, 一个事件). 我们为$\lambda$演算的变量保留符号$x,y,z$, 下一节我们将引入这个概念. [译注: 元语言和对象语言是相对的概念.]

第2.2节 计算上的意义

我们将以Heyting语义的角度重新检视自然演绎系统. 我们固定原子公式的解释以及量词的范围. 一个公式$A$将被看成是其所有可能的演绎构成的集合; 不说"$\delta$证明了$A$", 我们说"$\delta \in A$".

然后自然演绎的规则就以构造函数的特别方式显现: 以$B_1,\dots ,B_n$为假设的一个演绎$A$, 可以被看成是一个函数$t[x_1,\dots ,x_n]$, 其联系$b_i\in B_i$以结果$t[b_1,\dots ,b_n]\in A$. 实际上, 为了使得这种对应精确, 我们需要处理parcels of hypotheses: 相同的公式$B$可能在假设中出现多次, 而在相同的parcel中的两次$B$的出现应该对应于相同的变量.

以上的内容听起来似乎有些神秘, 但是通过一些例子, 其很快就会变得清晰起来.

第2.2.1小节 规则的解释

1. 仅由一个假设$A$构成的演绎由表达式$x$表示, 其中$x$是代表$A$的一个元素的变量. 之后, 若还有$A$的出现, 我们将选择相同的$x$, 或者另外一个变量, 这取决于这些出现是否在相同的parcel之中.
2. 如果一个演绎由两个演绎通过$\wedge \mathcal{I}$得到, 并且这两个演绎分别对应于$u[x_1,\dots ,x_n]$和$v[x_1,\dots ,x_n]$, 那么我们联系该演绎以序对$⟨u[x_1,\dots ,x_n],v[x_1,\dots ,x_n]⟩$, 这不过是因为对于合取的证明是一个序对. 我们刚才使得$u$和$v$依赖于相同的变量; 的确, 对于$u$和$v$的变量的选择是相互关联的, 因为某些parcels of hypotheses应该是同一个.
3. 如果一个演绎以$\wedge 1\mathcal{E}$作结, 并且$t[x_1,\dots ,x_n]$与立即子演绎相对应, 那么我们就将我们的证明与${\pi }^{1}t[x_1,\dots ,x_n]$相关联. 此即第一投影, 这不过是因为$t$作为对于合取的证明应该是一个序对. 类似地, $\wedge 2\mathcal{E}$和第二投影${\pi }^2$有关.
   尽管不是很形式化, 但是考虑以下基础等式是必要的:$${\pi }^1⟨u,v⟩=u,{\pi }^2⟨u,v⟩=v,⟨{\pi }^{1}t,{\pi }^{2}t⟩=t$$这些等式是逻辑学和计算机科学之间的对应的本质.
4. 如果一个演绎以$\Rightarrow \mathcal{I}$作结, 令$v$是与立即子演绎相关联的项; 这个立即子演绎在parcels of hypotheses的层次上是被无歧义地确定的, 这是在说一整个$A$-parcel都被discharged了. 如果$x$是一个与该parcel相关联的变量, 那么我们就有了一个函数$v[x,x_1,\dots ,x_n]$. 我们将我们的演绎与函数$t[x_1,\dots ,x_n]$相关联, 其将每个$A$的参数$a$映射至$v[a,x_1,\dots ,x_n]$. 我们所用的记号是$\lambda x.v[x,x_1,\dots ,x_n]$, 其中$x$是被绑定的变量.
   我们应该观察到绑定(binding)对应于discharge.
5. 以$\Rightarrow \mathcal{E}$作结的演绎的情况由考虑两个函数$t[x_1,\dots ,x_n]$和$u[x_1,\dots ,x_n]$处理, 其分别对应于两个立即子演绎.

第3章 Curry-Howard同构

我们已经看到Heyting的想法在自然演绎的框架之下执行得非常好. 我们将建立一个类型化项 (typed term) 的形式系统以讨论藏在证明背后的泛函对象. 这个系统的意义是藉由我们已经写下的泛函方程给出的. 实际上, 这些方程可以用两种不同的方式阅读, 这再次强化了涵义和指称之间的二分:

• 作为定义了项的相等性的等式, 换言之即指称的相等 (静态观点).
• 作为重写规则, 其允许我们通过规约至规范形式来计算项. 这是一种操作性的, 动态的观点, 而且对于逻辑学的此方面而言, 这是唯一真正带来丰富结果 (fruitful) 的观点.

当然, 第二种观点和第一种比起来有欠发展, 至少对于逻辑学是这样! 例如, 程序的指称语义 (例如, Scott语义) 有很多: 对于这种语义, 程序的执行过程中没有东西会发生变化. 另一方面, 几乎没有任何打磨精致的程序的操作语义 (我们排除只是粗糙重述迈向规范形式的步骤的ad hoc语义). 建立真正的算法的操作语义或许是计算机科学中最重要的问题.

类型和命题之间的对应在[3]之中建立起来.

第3.1节 lambda演算

第3.1.1小节 类型

当我们以Heyting的精神思考证明, 公式就成为了类型. 具体来说, 类型如下:

1. 原子类型$T_1,\dots ,T_n$是类型.
2. 如果$U$和$V$是类型, 那么$U\times V$和$U\to V$是类型.
3. (暂时)仅有的类型都是通过1和2得到的.

这与命题演算的$(\wedge ,\Rightarrow )$相对应: 原子命题写作$T_i$, $\wedge$成为$\times$, $\Rightarrow$成为$\to$.

第3.1.2小节 项

证明就成了项. 更准确地说, $A$的一个证明 ($A$作为公式) 成为一个具有类型$A$的项 ($A$作为类型). 具体来说, 项如下:

1. 变量$x_0^T,\dots ,x_n^T,\dots$是具有类型$T$的项.
2. 如果$u$和$v$分别是具有类型$U$和$V$的项, 那么$⟨u,v⟩$是具有类型$U\times V$的项.
3. 如果$t$是具有类型$U\times V$的项, 那么${\pi }^{1}t$和${\pi }^{2}t$分别是具有类型$U$和$V$的项.
4. 如果$v$是具有类型$V$的一个项并且$x_n^U$是一个具有类型$U$的变量, 那么$\lambda x_n^U.v$是一个具有类型$U\to V$的项. 一般而言, 我们将假定我们已经解决了绑定变量的选取以及替换问题, 通过这样或那样的方法, 这允许我们不需要考虑绑定变量的名字, 想法在于绑定变量没有individuality.
5. 如果$t$和$u$分别是具有类型$U\to V$和$U$的项, 那么$tu$是具有类型$V$的项.

第3.2节 指称上的意义

类型代表了某种正在被讨论的对象. 例如, 一个具有类型$U\to V$的对象是一个从$U$到$V$的函数, 一个具有类型$U\times V$的对象是一个序对, 由一个$U$的对象和一个$V$的对象构成. 原子类型的含义是不重要的, 其依赖于上下文.

第3.3节 操作性的意义

一般来说, 项代表程序. 程序的目的在于计算其指称, 或者至少是将指称置于一种便利的形式. 程序的类型被视为一种描述(specification), 即程序(抽象地)做了什么. 先验地说这是一种具有形式"这个程序计算两个整数之和"的评论.

第3.4节 转换

一个项被称为规范的, 如果没有其子项具有形式:$${\pi }^1⟨u,v⟩{\pi }^2⟨u,v⟩(\lambda x_n^U.v)u$$

第3.5节 对于同构的描述

第4章 规范化定理 (正则化定理)

本章关心的是确保类型化$\lambda$演算能够在计算上表现良好的两个结果. 规范化定理提供了规范形式的存在性, 而与此同时Church-Rosser性质保证了其唯一性. 实际上, 对于后者而言, 我们仅是简单陈述其内容但不加以证明, 因为其确非类型论的内容, 而且在许多文献中都有很好的讲解了, 例如[1].

规范化定理具有两种形式:

• 弱形式 (存在某个规范化的能够终止的策略), 这将在本章中进行证明.
• 强形式 (所有可能的规范化策略都将终止), 这在第6章中证明.

第4.1节 Church-Rosser性质

这个性质表达了规范形式的唯一性, 这独立于其存在性. 实际上, 它对于其他演算来说也有意义, 例如无类型$\lambda$演算, 在无类型的$\lambda$演算里规范化定理不成立.

Church-Rosser定理

第4.2节 弱规范化定理

这个结果陈述了每个项的规范形式的存在性, 当然它必然也是唯一的. 其立即的推论在于指称相等的可判定性.

第4.3节 弱规范化定理的证明

第4.4节 强规范化定理

第5章 相继式演算

归功于Gentzen, 相继式演算是对于逻辑学的对称的最漂亮刻画. 其与自然演绎有着诸多类似之处, 但是不局限于直觉主义的情形.

这种演算一般来说被计算机科学家所忽略, 尽管其刻画了某些基础性的想法: 例如, Prolog这种语言是对于相继式演算的部分实现, 而自动定理证明领域使用的"tableaux"方法不过是这种演算的一个特殊情形. 换言之, 它浑然不觉地被许多人使用, 但是混杂了控制特性, 即编程设备 (programming device). 使得这一切运作的是相继式演算及其深刻的对称性, 而不是什么特别的技巧. 所以说, 若是不知道相继式演算的微妙之处, 是很难考虑, 例如, Prolog的理论的.

从算法的角度来说, 相继式演算没有Curry-Howard同构, 这是因为太多书写相同证明的方式. 这阻止了我们将其当作类型化$\lambda$演算使用, 尽管我们瞥见了某种类似物的深层结构, 可能与并行有关. 但是, 它需要对于句法的新方法, 例如带有多个结论的自然演绎.

第5.1节 演算

第5.1.1小节 相继式

一个相继式是一个表达式$\underset{\_}{A}⊢\underset{\_}{B}$, 其中$\underset{\_}{A}$和$\underset{\_}{B}$是公式的有限序列$A_1,\dots ,A_n$和$B_1,\dots ,B_m$.

幼稚的(指称性)解释在于$A_i$的合取推出了$B_j$的析取, 特别地

• 如果$\underset{\_}{A}$为空, 那么相继式就断言了$B_j$的析取;
• 如果$\underset{\_}{A}$为空并且$\underset{\_}{B}$就是$B_1$, 那么它断言了$B_1$;
• 如果$\underset{\_}{B}$为空, 那么它断言了$A_i$的合取的否定;
• 如果$\underset{\_}{A}$和$\underset{\_}{B}$均为空, 那么它断言了一个矛盾.

第5.1.2小节 结构规则

这些规则, 似乎什么也没说, 强制规定了管理"槽"的一种特定方式, 在槽中人们书写公式. 规则如下, 它们是:

1. 交换规则$$\frac{\underset{\_}{A},C,D,\underset{\_}{A^{\prime }}⊢\underset{\_}{B}}{\underset{\_}{A},D,C,\underset{\_}{A^{\prime }}⊢\underset{\_}{B}}\mathcal{L}\mathsf{X}\frac{A⊢\underset{\_}{B},C,D,\underset{\_}{B^{\prime }}}{A⊢\underset{\_}{B},D,C,\underset{\_}{B^{\prime }}}\mathcal{R}\mathsf{X}$$这些规则表达了逻辑的交换性, 通过允许符号$⊢$每一边的公式进行置换.
2. 削弱规则$$\frac{\underset{\_}{A}⊢\underset{\_}{B}}{\underset{\_}{A},C⊢\underset{\_}{B}}\mathcal{L}\mathsf{W}\frac{\underset{\_}{A}⊢\underset{\_}{B}}{\underset{\_}{A}⊢C,\underset{\_}{B}}\mathcal{R}\mathsf{W}$$正如名字所暗示的那样, 其允许将相继式代替以一个更弱的相继式.
3. 收缩规则$$\frac{\underset{\_}{A},C,C⊢\underset{\_}{B}}{\underset{\_}{A},C⊢\underset{\_}{B}}\mathcal{L}\mathsf{C}\frac{\underset{\_}{A}⊢C,C,\underset{\_}{B}}{\underset{\_}{A}⊢C,\underset{\_}{B}}\mathcal{R}\mathsf{C}$$表达了合取与析取的幂等性.

事实上, 与流行的认知相反, 这些规则才是整个演算里最重要的部分. 这是因为, 在还没有写下任何一个逻辑符号之前, 我们实际上就已经能够确定逻辑操作的未来行为. 尽管这些规则从指称的角度来看是显然的, 但是我们应该从操作的角度仔细检视这些规则, 特别是收缩.

第5.1.3小节 直觉主义的情形

第5.1.4小节 "相等"群

第5.1.5小节 逻辑规则

传统上人们认为逻辑是一种形式游戏, 一连串或多或少有些随意的公理和规则. 相继式演算 (当然自然演绎也是) 表明实际上完全不是这么一回事: 人们可以自娱自乐地发明他们自己的逻辑操作, 但是这些逻辑操作不得不尊重左/右对称, 否则的话他们发明的就只是一种毫无趣味的逻辑暴行. 具体来说, 对称指的是我们可以消除切规则.

第5.2节 无切系统的一些性质

第6章 强规范化定理

本章我们将证明简单类型$\lambda$演算的强规范化定理, 但是既然

第7章 Gödel的系统T

第7.1节 演算

第7.1.1小节 类型

第3章中我们允许额外的常量类型; 现在我们将描述两种这样的类型, 分别是$\mathsf{Int}$ (整数) 和$\mathsf{Bool}$ (布尔).

译注: 根据第1章的原注, 本书的整数都是指自然数.

第7.1.2小节 项

除了常见的五种, 对于$\mathsf{Int}$和$\mathsf{Bool}$存在特定的scheme. 我们保持了使用引入/消去术语, 因为这些scheme还将出现在之后的$\mathbf{F}$之中.

1. $\mathsf{Int}$引入:
   • $\mathsf{O}$是一个具有类型$\mathsf{Int}$的常量;
   • 如果$t$具有类型$\mathsf{Int}$, 那么$\mathsf{S}t$具有类型$\mathsf{Int}$.
2. $\mathsf{Int}$消去: 如果$u,v,t$分别具有类型$U,U\to (\mathsf{Int}\to U),\mathsf{Int}$, 那么$\mathsf{R}uvt$具有类型$U$.
3. $\mathsf{Bool}$引入: $\mathsf{T}$和$\mathsf{F}$具有类型$\mathsf{Bool}$.
4. $\mathsf{Bool}$消去: 如果$u,v,t$分别具有类型$U,U,\mathsf{Bool}$, 那么$\mathsf{D}uvt$具有类型$U$.

第7.1.3小节 意图的含义

1. $\mathsf{O}$和$\mathsf{S}$分别是零元和后继函数.
2. $\mathsf{R}$是递归算子: $\mathsf{R}uv0=u$, $\mathsf{R}uv(n+1)=v(\mathsf{R}uvn)n$.
3. $\mathsf{T}$和$\mathsf{F}$是真值.
4. $\mathsf{D}$是"if ... then ... else": $\mathsf{D}uv\mathsf{T}=u$, $\mathsf{D}uv\mathsf{F}=v$.

译注: 在某种意义上这里有点符号滥用.

第7.1.4小节 转换

除了经典的redex, 我们加入了:$$\mathsf{R}uv\mathsf{O}⇝u$$$$\mathsf{R}uv(\mathsf{S}t)⇝v(\mathsf{R}uvt)t$$$$\mathsf{D}uv\mathsf{T}⇝u$$$$\mathsf{D}uv\mathsf{F}⇝v$$

第7.2节 规范化定理

在$\mathbf{T}$中, 所有的规约序列都是有限的, 并将导向相同的规范形式.

第7.3节 表达力: 例子

第7.3.1小节 布尔

典型的例子是逻辑联结词:$$\mathsf{neg}(u)=\mathsf{D}\mathsf{F}\mathsf{T}u\mathsf{disj}(u,v)=\mathsf{D}\mathsf{T}vu\mathsf{conj}(u,v)=\mathsf{D}v\mathsf{F}u$$例如, $\mathsf{disj}(\mathsf{T},x)⇝\mathsf{T}$和$\mathsf{disj}(\mathsf{F},x)⇝x$. 但是, 从另一方面来说, 如果遇到了表达式$\mathsf{disj}(x,\mathsf{T})$, 那么我们就不知道该做什么了.

问题. 有没有一种可能定义另外一种析取, 但它是对称的?

在第9.3.1小节的时候, 我们将看到, 根据语义方法, 可以说明不存在具有类型$\mathsf{Bool},\mathsf{Bool}\to \mathsf{Bool}$的项$G$满足$$G⟨\mathsf{T},x⟩⇝\mathsf{T}G⟨x,\mathsf{T}⟩⇝\mathsf{T}G⟨\mathsf{F},\mathsf{F}⟩⇝\mathsf{F}$$

第7.3.2小节 整数

首先我们必须表示整数: 选择用$\bar{n}={\mathsf{S}}^n\mathsf{O}$来表示整数$n$是显然的.

经典的函数可以用简单的递推关系定义 [虽然译者觉得应该说是递归?]. 让我们给出加法的例子: 我们需要从我们已经熟知的定义方程开始:$$x+\mathsf{O}=xx+\mathsf{S}y=\mathsf{S}(x+y)$$

考虑$t[x,y]=\mathsf{R}x(\lambda z^{\mathsf{Int}}.\lambda {z^{\prime }}^{\mathsf{Int}}.\mathsf{S}z)y$:$$t[x,\mathsf{O}]⇝xt[x,\mathsf{S}y]⇝(\lambda z^{\mathsf{Int}}.\lambda {z^{\prime }}^{\mathsf{Int}}.\mathsf{S}z)(t[x,y])y⇝\mathsf{S}t[x,y]$$这表明我们可以将$t[x,y]$当作$x+y$的一个定义.

通过类似这种风格的简单练习, 我们可以自娱自乐地定义乘法, 幂, 前继, 等等.

整数上的谓词当然也可以被定义, 例如$$\mathsf{null}(\mathsf{O})=\mathsf{T}\mathsf{null}(\mathsf{S}x)=\mathsf{F}$$给出了$$\mathsf{null}(x)\stackrel{\mathrm{def}}{=}\mathsf{R}\mathsf{T}(\lambda z^{\mathsf{Bool}}.\lambda {z^{\prime }}^{\mathsf{Int}}.\mathsf{F})x$$这允许我们将一个特征函数 (类型$\mathsf{Int}$) 转换为一个谓词 (类型$\mathsf{Bool}$).

这些例子都没有严肃地运用高阶类型. 然而, 随着在递归中使用的类型的增加, 越来越多的函数变得可以表达. 例如, 如果$f$具有类型$\mathsf{Int}\to \mathsf{Int}$, 我们可以定义类型为$\mathsf{Int}\to \mathsf{Int}$的$\mathsf{it}(f)$为$$\mathsf{it}(f)x=\mathsf{R}\bar{1}(\lambda z^{\mathsf{Int}}.\lambda {z^{\prime }}^{\mathsf{Int}}.fz)x$$那么$\mathsf{it}(f)\bar{n}$就是$f^n\bar{1}$了. 作为具有类型$(\mathsf{Int}\to \mathsf{Int})\to (\mathsf{Int}\to \mathsf{Int})$的对象, 函数$\mathsf{it}$是:$$\lambda x^{\mathsf{Int}\to \mathsf{Int}}.\mathsf{it}(x)$$

很容易看出来, 通过某个合理的函数$f_0$的有限迭代, 我们可以超越每个原始递归函数. 例如, 给定$n$返回${\mathsf{it}}^n{f}_0$的函数 (Ackermann函数) 就要比所有原始递归函数增长得更快.

译注: 上面这段话不是很理解, 因为我不知道什么是$f_0$.

这种函数在$\mathbf{T}$中很容易定义, 只要我们使用一个复杂类型上的递归, 例如$\mathsf{Int}\to \mathsf{Int}$: 取$\mathsf{R}{f}_0(\lambda x^{\mathsf{Int}\to \mathsf{Int}}.\lambda z^{\mathsf{Int}}.\mathsf{it}(x))y$, 其对于$y=\mathsf{O}$将被规范化为$f_0$, 对于$\bar{n}$将被规范化为${\mathsf{it}}^n{f}_0$.

为了给本小节作结, 我们应该指出$\mathsf{R}uvt$中的$v$的第二个参数实际上经常是不用的. 可能有人更倾向于使用迭代子$\mathsf{It}$而不是$\mathsf{R}$, 其应用于具有类型$T$的$u$, 具有类型$T\to T$的$v$, 以及具有类型$\mathsf{Int}$的$t$, 而规则是:$$\mathsf{It}uv(\mathsf{S}t)⇝v(\mathsf{It}uvt)$$

满足等式

第7.4节 表达力: 结果

第8章 coherence空间

第9章 T的指称语义

第10章 自然演绎中的和

第11章 系统F

第12章 和的coherence语义

第13章 切消 (Hauptsatz)

第14章 F的强规范化性质

第15章 表示定理

附录A: 系统F的语义

附录B: 什么是线性逻辑?

参考文献