类型论中定义展开的精细控制：基于扩展类型的新型机制及其在证明助理中的应用

《Mathematical Structures in Computer Science》：Controlling unfolding in type theory

本文针对依赖类型理论中定义展开控制的难题，提出了一种基于扩展类型（extension types）的新型机制。研究人员设计了一种表面语言，允许用户选择性、局部地展开定义，并通过将其精化到带有命题符号和扩展类型的核心演算来证明其合理性。该研究解决了传统证明助理中定义透明性与不透明性之间的固有矛盾，在cooltt证明助理中实现了可控展开功能，为提升证明的模块化、可维护性和性能提供了重要工具。

　　

在依赖类型理论和证明助理的世界里，一个长期存在的难题是如何巧妙地控制定义的展开。定义展开是类型检查的基石，它允许系统静默地验证许多证明义务，例如，将长度为1+1的列表自动识别为长度为2的列表。然而，过度展开会导致证明脆弱不堪，微小的定义改动就可能引发大规模的类型错误；同时，展开复杂的定义也会使证明状态变得难以阅读，并严重影响类型检查的性能。传统的解决方案，如Agda的abstract块或Coq的Opaque命令，往往采取非此即彼的极端策略：要么让定义完全透明（始终展开），要么让其完全 opaque（永不展开）。这种僵化的控制方式无法满足实际开发的需求，因为要推理关于一个函数，我们必须展开它，但为了模块化和性能，我们又希望在其他时候保持其抽象。

为了破解这一矛盾，Daniel Gratzer、Jonathan Sterling、Carlo Angiuli、Thierry Coquand和Lars Birkedal在《Mathematical Structures in Computer Science》上发表了他们的研究成果“Controlling unfolding in type theory”。他们提出了一种名为“可控展开”的新机制，旨在为定义展开提供前所未有的精细控制。该研究的核心思想是让定义默认不展开，但允许用户根据需要在局部范围内选择性地展开它们，从而在便利性、模块化和性能之间取得最佳平衡。

为了回答如何实现这种可控展开的问题，研究人员开展了一项构建新型表面语言及其精化语义的理论与实践研究。他们得出的核心结论是，通过引入语言层面的原语（如unfold表达式和unfolds声明），并利用首次在同伦类型论背景下引入的扩展类型（{A | p ? ap}）将其精化到一个核心演算中，可以构建一个既灵活又可靠的系统。这项研究的意义在于，它不仅提供了一种实用的编程语言特性，而且通过建立核心演算的正规化定理，确保了该机制的可靠性和类型检查的可判定性，其实现已成功集成到实验性的cooltt证明助理中，并启发了Agda的独立实现。

研究人员为开展此项研究，主要运用了以下几个关键技术方法：首先，他们设计了一种扩展马丁-洛夫类型论（MLTT）的核心演算TTP，引入了命题符号和扩展类型。其次，他们开发了将带有可控展开原语的表面语言精化到该核心演算的算法。最关键的是，他们利用合成Tait可计算性（STC）技术，构造性地证明了核心演算的正规化定理，从而确保了精化算法的可实施性。这项研究是在cooltt证明助理这一具体系统中实现和验证的。

表面语言与示例

研究首先展示了一个类Agda的表面语言。在该语言中，定义（如自然数加法+）默认是不透明的。用户可以通过(⊕) unfolds (+)这样的声明，指定在定义⊕（向量连接）时展开+。这使得在定义⊕时，类型检查器能够利用+的计算规则（如ze + n = n），从而简化证明目标。这种展开是传递的，例如，如果展开⊕（其定义中使用了+），那么+也会被自动展开，这是保证主体约简所必需的。

精化到核心演算

研究的核心在于将表面语言构造精化到一个名为TTP的核心类型论中。TTP扩展了MLTT，引入了命题符号p（来自一个有余格结构P）、依赖积{p} A（在假设p为真时成立的A）以及扩展类型{A | p ? a_p}（当p为真时，其元素与a_p定义相等的A的类型）。每个用户定义?都被精化为一个核心常量，其类型是一个扩展类型{A | ?_? ? δ_?}，其中?_?是一个命题符号（表示“应展开?”），δ_?是在假设?_?为真的情况下定义的项。? unfolds κ?;…;κ?声明则被精化为规定?_?蕴含?_κ? ∧ … ∧ ?_κ?。

正规化证明

为了确保精化算法可行（因为精化需要判断核心语言中的类型相等性），研究团队为核心演算TTP建立了正规化定理。证明采用了Sterling提出的合成Tait可计算性（STC）方法，该方法在Grothendieck拓扑斯中语义地进行。他们构造了一个“可计算性空间”的闭包拓扑斯G，其中对象是“粘合”在一起的来自对象空间（初始模型I）和元空间（原子替换模型A）的数据。通过在这个粘合模型中解释TTP，他们定义了一个正规化代数，从而能够提取项和类型的正规形式。该证明是完全构造性的，并纠正了Sterling早期博士论文中在处理宇宙时的一个错误。

实现

研究团队在实验性证明助理cooltt中实现了可控展开机制。实现利用了cooltt对部分元素和扩展类型的现有支持，并修改了Kado库以支持维度变量的不等式，从而能够处理命题符号之间的蕴涵关系。实现后的功能允许用户使用unfold表达式和unfolds声明来精细控制定义的展开。

本研究成功提出并形式化了一种用于依赖类型理论中控制定义展开的新机制。其重要意义在于：首先，它解决了证明助理中长期存在的透明性与不透明性之间的权衡问题，提供了比现有方法（如Agda的abstract块或Coq的转换策略）更精细、更模块化且行为更可预测的解决方案。其次，该机制建立在扩展类型这一坚实的类型论概念之上，并通过精化和正规化定理得到了严格的理论保证，确保了其可靠性。最后，在cooltt中的实现证明了其可行性，并已启发了主流证明助理（Agda）的跟进，显示了其潜在的重大实用价值和影响力，有望显著提升大型形式化数学库的工程化水平。