A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

技术摘要：关于非谓词纯类型系统一致性的机器检查证明

问题与背景
本文旨在解决类型论机械化过程中的挑战，特别关注纯类型系统（PTS）的元理论属性。形式化处理替换（substitution）和 $\beta$-归约（$\beta$-reduction）的一个核心难点在于如何处理变量重命名以防止名称捕获。传统的定义（如 Curry-Feys）由于重命名步骤是非原始递归的，需要基于项长度的良基归纳法（well-founded induction），这使得机械化变得困难。其他的替代方案，如 de Bruijn 指数（dBI）、局部命名语法（locally nameless syntax）以及高阶抽象语法（HOAS），虽然提供了解决方案，但也各自带来了缺陷：dBI 对人类可读性不友好；局部命名语法需要“污染”元理论结果的良构谓词（well-formedness predicates）；而 HOAS 则往往会阻碍生成可执行代码或提出可判定性问题。

作者旨在评估一种保留经典语法（使用命名变量）并利用 Stoughton 的同步替换（Stoughton's simultaneous substitutions）的方法的可行性。该方法通过单次结构递归，在进行替换的同时对绑定变量进行重命名，从而避免了在大多数证明中需要基于项长度的良基归纳法。

方法论
本研究完全使用 Agda (v2.6.2.2) 及其标准库进行机器检查开发。该方法依赖于以下核心组件：

1. Stoughton 的同步替换： 替换被定义为从变量到 $\lambda$-项的函数（$Sub = V \to \Lambda$）。操作 $M \bullet \sigma$ 通过结构递归定义。对于 $\lambda$-抽象和 $\Pi$-类型，绑定变量会被重命名为一个由函数 $X$ 选出的新名称 $y$，并且替换映射会更新，将旧的绑定变量映射到这个新名称。这确保了每个抽象只需要一次递归调用，从而保持了原始递归性。
2. $\alpha$-交换关系（$\alpha$-Commutative Relations）： 作者开发了一套与 $\alpha$-转换交换的关系理论。如果关系 $S$ 是 $\alpha$-交换的，则若 $M \sim_\alpha N$ 且 $N S P$，则存在一个 $Q$ 使得 $M S Q$ 且 $Q \sim_\alpha P$。这一框架允许作者清晰地处理直到 $\alpha$-转换的合一性（confluence），避免了在其他形式化中常见的引理重复问题。
3. Takahashi 对合一性证明的修订： 本文没有采用原始的 Tait 和 Martin-Löf 证明，而是采用了 Takahashi 使用并行归约（parallel reduction, $\Rightarrow$）的修订版本。作者在定义并行归约时，其归约步骤中不包含显式的 $\alpha$-转换规则，而是依靠五边形性质（pentagon property，即在 $\alpha$-转换意义下对钻石性质的推广）来证明合一性。
4. 归一化假设： 关于一致性的证明假设所讨论的特定 PTS 是归一化的（即每个类型良好的项都是弱归约的）。作者指出，由于 Agda 在元语言层面缺乏谓词性（impredicativity），在 Ag Agda 中证明此类非谓词系统的归一化性可能是无法实现的。

主要贡献
论文展示了对三个主要元理论属性的形式化证明：

1. $\beta$-归约的合一性： 作者证明了 PTS 底层语法的 Church-Rosser 定理。通过利用 $\alpha$-交换关系理论和 Takahashi 的并行归约，他们确立了并行归约的星号闭包（star closure）与多步 $\beta$-归约一致，并满足五边形性质。
2. 类型保持（Subject Reduction, SR）： 论文形式化了归约下的类型保持。遵循 McKinna 和 Pollack 的思路，作者将归约扩展到上下文，并证明了一个关于上下文有效性以及主体类型保持的同步定理。这包括证明积注入性（product injectivity），这是反转引理（inversion lemma）的一个关键步骤。
3. 非谓词 PTS 的一致性： 作者证明了对于特定的非谓词 PTS 子类（满足特定公理和规则的类，例如 $(\ast, \square) \in \mathcal{A}$ 且 $(\square, \ast, \ast) \in \mathcal{R}$），类型 $\Pi[x : s]x$（在 Curry-Howard 对应下代表谬误/Falsehood）在空上下文中是无解的。该证明扩展了 Coquand 的纸面证明（针对构造演算 CC）。它依赖于归一形式和中性形式的归纳定义之可靠性与完备性、反转引理以及假设的归一化性质。

结果与评估

• 形式化规模： 整个开发工作包含约 4,300 行代码 (LoC)，其中 3,000 行 LoC 归功于之前工作中关于 Stoughton 替换和 PTS 语法的底层框架。
• 比较： 作者将其工作与使用 de Bruijn 指数的实现（Barras 和 Werner，约 2,900 LoC）以及局部命名语法的实现（Aydemir 等人，约 4,800 LoC）进行了比较。他们认为其方法在规模上具有可比性，但在处理使用的语法方面具有更高的透明度，因为它更接近非正式的数学呈现（例如，弱化引理的写法与经典符号几乎完全一致）。
• 可行性： 结果表明，使用经典语法和同步替换的方法对于依赖类型理论是可行的。作者指出，仅有少数引理需要用到良基归纳法，且代码规模并未出现“爆炸”。

意义与主张
论文声称，使用 Stoughton 替换的方法与类似的发展相比，在处理元理论问题（特别是处理 $\alpha$-转换方面）时提供了“更清晰的呈现和处理”。作者断言，由于避免了打开项（opening terms）和手动管理新鲜参数带来的“符号杂乱”，其方法对人类读者而言比局部命名或 de Bruijn 方法更加透明。

这项工作的意义在于证明，只要假设归一化，实现非谓词系统的一致性的机器检查证明是可能的，且无需放弃经典语法。作者谦虚地承认，由于 Gödel 不完备定理的影响，在 Agda 中实现此类非谓词理论的完整归一化证明在证明论强度上可能是无法实现的，但一致性证明本身仍是构建此类系统正确性保证（correct-by-construction）类型检查算法的重要一步。这项工作验证了该框架在未来依赖类型理论形式化中的实用价值。