无规范化的定义性反转
Definitional Inversion, Without Normalisation
浏览论文内容
中文总结 AI 辅助
基于域理论提出新证明技术，用于证明依赖类型系统的定义性反转性质，与规范化无关，能在特定系统中建立类型构造函数单射性，还适用于非规范化类型理论及相关项目，并展示了方法及扩展。
中文摘要 AI 辅助
我们贡献了一种基于域理论的新证明技术，用于证明依赖类型系统的关键元理论性质：定义性反转性质，即类型构造函数的单射性和无混淆性。此证明技术与规范化无关，甚至适用于Martin-Löf原始类型理论的“类型内类型”规则。我们的证明首次在存在η律的情况下为这样的系统建立了类型构造函数的单射性。更一般地，该技术适用于如Idris、Lean或依赖Haskell等底层类型理论已知是非规范化的系统的元理论，以及如MetaRocq或Lean4Lean等项目，在这些项目中哥德尔第二不完备定理意味着我们无法证明对象逻辑本身的规范化。我们在一个小型类型理论上展示了该方法，然后解释了它如何扩展到更复杂的扩展。
英文摘要
We contribute a new proof technique, based on domain theory, to prove key meta-theoretic properties of dependent type systems: definitional inversion properties, i.e. injectivity and no-confusion of type constructors. This proof technique is independent of normalisation, and indeed applies even for the "type-in-type" rule of Martin-Löf's original type theory. Our proof is the first to establish injectivity of type constructors for such a system in the presence of $η$ laws. More generally, the technique is motivated by, and intended for, the metatheory of systems such as Idris, Lean, or dependent Haskell, whose underlying type theory is known to be non-normalising, as well as projects such as MetaRocq or Lean4Lean, where Gödel's second incompleteness theorem means we cannot show normalisation of the object logic in itself. We showcase the method on a small type theory, then explain how it extends to more ambitious extensions.
