Definitional Inversion, Without Normalisation

想象一下，你正在建造一座宏大的魔法图书馆，其中的每一本书都是一个数学证明，而书架本身则是由逻辑构成的。这就是**依赖类型系统（dependent type systems）**的世界，它是像 Lean 这样的现代证明助手以及编程语言（如 Idris）背后的秘密引擎。在这个世界里，规则极其严格：如果你试图把一只“猫”放在贴着“数字”标签的书架上，图书馆的安全系统（类型检查器）应该立即发出“错误！”的尖叫并阻止你。这种安全性依赖于一个概念——定义相等性（definitional equality），这是图书馆判断两个事物本质上是否相同的方式。例如，“正方形”是否仅仅是“四条边相等的矩形”？如果系统判定是的，它就会将它们视为同一物。

然而，检查这些规则非常棘手。传统上，为了证明图书馆是安全的，数学家必须展示每一本书都能被简化到其最简单、最基础的形式（这个过程称为规范化/归约化，normalization）。但许多现代且强大的库被设计成是无限的或自指的，这意味着它们无法被简化到一个最终的终点。这就像试图压平一个分形；你会不断发现更多的细节。长期以来，如果一个系统无法被简化，我们就无法证明它是安全的。本文介绍了一种新的方法，无需先将分形压平，即可检查图书馆的安全性。

---

无限谜题与魔镜

将依赖类型系统想象成一个巨大的、自我检查的谜题。这些碎片是类型（如“数字”或“函数”），目标是确保当你把两个碎片拼在一起时，它们能完美契入。这个谜题中最关键的规则是定义反转（definitional inversion）。它是这样一种逻辑：“如果两个复杂的结构看起来相同，那么它们的组成部分也必须相同。”例如，如果你有两个完全相同的函数类型，那么它们的输入类型和输出类型也必然相同。这至关重要，因为它允许计算机安全地将复杂的代码分解为更小的部分，而不会产生混乱。

几十年来，证明这些碎片能够契合的唯一方法是使用一种叫做合一性（confluence）的方法（检查不同的简化路径是否会导致相同的结果）或逻辑关系（logical relations）（一种比较项之行为的复杂方法）。但这些旧工具遇到了瓶颈。当加入某些“外延性”规则（例如 $\eta$-法则，即规定一个函数完全由它的行为而非其写法来定义）时，合一性就会失效。而逻辑关系通常要求系统必须是“规范化的”（即能够停止简化），这排除了许多强大的、允许无限循环或自指类型的现实世界编程语言。

新方法：可能性的地图

作者们（一个由计算机科学家和数学家组成的团队）提出了一种基于域理论（domain theory）的新策略。他们不再试图强迫谜题碎片简化成单一的最终形状，而是构建了一张所有可能行为的地图。

想象你在黑暗的森林中试图识别一个神秘生物。

• 旧方法： 你等待生物停止移动并显现出其真实的、最终的形态。如果这个生物永远不停下移动（因为是一个无限循环），你就无法识别它，森林也就变得不安全。
• 新方法： 你不等它停止。相反，你观察它的足迹。你注意到它留下了一个“左脚”印记，然后是一个“右脚”印记，接着又是一个“左脚”印记。即使这个生物永远不停下行走，你仍然可以通过观察它的步法模式来推断出它的形状。

在论文的语言中，这些“足迹”被称为紧元素（compact elements）或有限观测（finite observations）。作者构建了一个数学“域”（一个结构化空间），在这里，每个类型不由一个最终答案表示，而是由关于它的所有有限观测集合来表示。他们使用一种称为**有限投影算子（finitary projectors）**的技术，将这个域切分成易于处理的块。

他们的发现

利用这种“足迹”方法，团队成功证明了即使在以下系统中，定义反转依然成立：

1. 永不停止简化（非规范化）的系统，例如带有“类型包含类型（type-in-type）”规则的系统（即类型可以包含自身）。
2. 包含 $\eta$-法则的系统，这些规则虽然让函数和对（pairs）的行为更加直观，但会破坏传统的证明方法。

他们在一种名为 MLTT$\eta$（带有 $\eta$-法则的马丁-洛夫类型论）的小型核心版本上演示了这一点。他们证明了即使在这个混乱且可能无限的系统中，如果两个类型相等，它们的构建模块也必然相等。这是一个重大突破，因为它证明了即使系统允许变得杂乱无章和无限，其“安全网”依然有效。

这为什么重要

作者们不仅仅是为一个微小的玩具系统解开了谜题；他们展示了他们的方法是稳健的（robust）。他们扩展了证明以包含：

• 依赖和（dependent sums）（数据对）。
• 单位类型（unit types）（只有一个值的类型）。
• 不动点组合子（fixed-point combinators）（允许无限递归的工具）。
• 带有模式匹配的自然数。
• 恒等类型（identity types）（证明两件事是相同的）。
• 证明无关命题（proof-irrelevant propositions）（其中证明的内容并不重要，只要证明存在即可）。

他们甚至为“严格命题的宇宙”构建了一个模型，表明其技术可以处理像 Lean、Agda 和 Rocq 这样具有复杂特征的现实世界工具。

局限性与未来

论文非常明确地说明了它没有做的事情。它并没有证明这些系统是“规范化的”（即它们总是会停止）。事实上，它明确地适用于那些不会停止的系统。它也没有以同样的方式解决“中性项（neutrals）”（尚未填充变量的变量）的问题，尽管它暗示了未来可以如何解决。

作者们已经将他们的数学证明转化为了代码，并在三个不同的证明助手（Agda、Lean 和 Rocq）中进行了三次验证。这表明，他们的研究不仅是一个理论构想，更是一个实用的工具。

总结

这篇论文就像是递给魔法图书馆建设者一副新的眼镜。以前，他们只有在书籍是静态且完成的状态下才能检查图书馆的安全。现在，他们可以检查那些仍在编写中、或者正在进行无限自我引用的书籍的安全。通过关注可观测行为（足迹）而非最终目的地（停止），他们为验证我们所能想象到的最强大、最复杂且可能无限的类型系统打开了大门。这为“Lean4Lean”和“MetaRocq”等项目铺平了道路——在这些项目中，证明助手可以验证自身的代码，使我们用于构建数学和软件的工具变得更加值得信赖。