系统的性质

核心系统

下面的定理针对的是核心系统：图 3.1 的规则，加上第 13 章的宇宙，不含第二部分的常量。按 Barendregt 的说法，这是一个纯类型系统（Pure Type System）：构造演算（Calculus of Constructions）[Coquand 1988]，在其非谓词的 $\Sort{0}$ 之上加一层谓词宇宙的层级，接近 Luo 的扩展构造演算（Extended Calculus of Constructions）[Luo 1990]。前三条性质对每个函数式纯类型系统都成立 [Barendregt 1992]，而在存在非谓词性的情况下，强规范化要困难得多，需要 Girard 的可归约性候选（reducibility candidates）方法 [Girard 1972; Coquand 1988; Luo 1990]。本章末尾说明加入归纳类型后会有什么变化。

四条性质

一个项在转换意义下只有一个类型。$\Infer$ 依赖这一点：它要计算的答案只有一个，$\Check$ 可以放心地与之比较，不必担心另一棵推导会给出某个不可转换的不同类型。

良类型项的类型本身也是一个类型（或者是一个宇宙；宇宙按 T-Sort 也有类型，只是不必写成那种形式）。因此 $\Infer$ 的结果总能再交给 $\InferSort$，算法构造的上下文也始终保持良构。

计算保持类型，正是它为 T-Conv 以及“通过规范化判定相等”这一整套策略提供了依据：归约一个项永远不会使它离开自己的类型，所以比较范式，比较的正是该比较的东西。

每个良类型项都能到达范式，无论按什么顺序归约。这是最深刻的一条：$\Whnf$、$\Normalize$，从而 $\IsDefEq$ 和 $\Infer$，在良类型输入上终止都是因为它；下一节还会说明，一致性同样建立在它之上。

四条性质按一种确定的模式支撑着两项保证，如下图所示：箭头读作“为……所需”。

这些性质合起来，给出了我们对一个内核所要求的两项保证。

• 可判定性. 算法 5.1 在每个输入上都终止，所以一个证明是否正确总能被判定。
• 一致性. 没有封闭项能证明 False。

一致性

论证分两半，不看细节也能看出它的轮廓。

归结到范式. 由强规范化，这样的项 $t$ 会有范式 $n$；由类型保持性，$n$ 的类型不变。因此只需证明：没有任何处于范式的封闭项具有类型 $\tPi{P}{\Sort{0}}{P}$。全部困难都在这一步，因为它用到了定理 14.4。

分析范式. 范式项要么是宇宙、$\Pi$、$\lambda$，要么是一个变量作用于若干参数（称为中性项，neutral term）。类型为 $\Pi$ 的封闭范式项必定是 $\lambda$：它不可能是中性项，因为作用域内没有任何变量；而宇宙和 $\Pi$ 类型的类型是宇宙，不是 $\Pi$。于是 $n = \tLam{P}{\Sort{0}}{s}$，其中 $P : \Sort{0} \vdash s : P$ 且 $s$ 是范式。现在问 $s$ 能是什么：宇宙、$\Pi$ 或 $\lambda$ 的类型会是宇宙或 $\Pi$，而不是变量 $P$。中性项必须以作用域内的某个变量开头，而作用域内只有 $P$ 本身，其类型是 $\Sort{0}$：这个类型不是 $P$，所以 $s$ 不能是 $P$；它也不是函数类型，所以 $P$ 不能作用于任何东西。每种情形都不可能。

附录 D 严格地完成这一论证，包括上述情形分析默默用到的关于类型和转换的标准事实（生成引理、合流性、替换）。

加入归纳类型之后

第二部分的 ι 规则彼此不重叠，也不与 β 重叠，所以归约仍然合流。类型保持性、强规范化和一致性对归纳构造演算（Calculus of Inductive Constructions）都是已知结果 [Werner 1994]，而我们带归纳类型的系统只是它的一个小片段。上面的简短一致性论证本身已不再够用，因为范式现在还包括卡住的递归子应用，例如 $n$ 为变量时的 $\NatRec{0}\;M\;z\;s\;n$；一致性仍由强规范化导出，但需要对范式做更细致的分析，其中中性项也可以以常量为头部。

第 8 章的每一条接受条件都对应这一分析可能失败的一种方式：没有正性，ι 归约可能循环，强规范化就丢失了；没有宇宙条件，一个类型可以包含自己所在的宇宙，第 13 章的悖论就会卷土重来；没有对命题的消去限制，证明无关性（Lean 假定它成立）就会被推翻。

Lean 的完整理论带有定义性证明无关性、宇宙多态、商类型以及一般的嵌套归纳类型和互归纳类型，其元理论更为微妙；Carneiro 的论文 [Carneiro 2019] 是这方面的参考文献。但核心结构是一样的：强规范化加上范式分析。

练习