Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory
Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory
复制标题
证明相关的统一：仅与类型理论的公理进行依赖模式匹配
DOI：
10.1017/s095679681800014x
复制
发表时间：
2018
影响因子：
1.1
通讯作者：
Dominique Devriese
中科院分区：
文献类型：
--
作者：
Jesper Cockx;Dominique Devriese
依赖类型语言如Agda、Coq和Idris使用语法一阶统一算法通过依赖模式匹配来检查定义。然而，标准的统一算法隐含地依赖于诸如身份证明的唯一性和类型构造函数的内射性之类的原则。这些原则在许多类型理论中是不能接受的，特别是在新的和有前途的分支同伦类型理论中。因此，这些新理论中的程序和证明不能使用依赖模式匹配或其他依赖于统一的技术，因此更难编写，修改和理解。本文提出了一个证明相关的框架，在依赖类型设置的统一形式化推理。在这个框架中，统一规则不仅计算统一符，而且还以两组方程之间的等价形式计算相应的可靠性证明。通过以与证明相关的方式改写标准统一规则，它们保证了理论的可靠性。此外，它使我们能够安全地添加新的规则，可以利用方程类型之间的依赖关系，例如记录类型的eta-equality规则和解决等式证明之间方程的高维统一规则。使用我们的框架，我们实现了对Agda使用的统一算法的彻底改革。因此，我们能够用正式验证的统一规则取代以前的临时限制，修复了过程中的大量错误。在未来，我们可能还希望将新的原则与模式匹配相结合，例如，同伦类型理论引入的更高归纳类型。我们的框架还为此类扩展提供了坚实的基础。
Abstract Dependently typed languages such as Agda, Coq, and Idris use a syntactic first-order unification algorithm to check definitions by dependent pattern matching. However, standard unification algorithms implicitly rely on principles such as uniqueness of identity proofs and injectivity of type constructors. These principles are inadmissible in many type theories, particularly in the new and promising branch known as homotopy type theory. As a result, programs and proofs in these new theories cannot make use of dependent pattern matching or other techniques relying on unification, and are as a result much harder to write, modify, and understand. This paper proposes a proof-relevant framework for reasoning formally about unification in a dependently typed setting. In this framework, unification rules compute not just a unifier but also a corresponding soundness proof in the form of an equivalence between two sets of equations. By rephrasing the standard unification rules in a proof-relevant manner, they are guaranteed to preserve soundness of the theory. In addition, it enables us to safely add new rules that can exploit the dependencies between the types of equations, such as rules for eta-equality of record types and higher dimensional unification rules for solving equations between equality proofs. Using our framework, we implemented a complete overhaul of the unification algorithm used by Agda. As a result, we were able to replace previous ad-hoc restrictions with formally verified unification rules, fixing a substantial number of bugs in the process. In the future, we may also want to integrate new principles with pattern matching, for example, the higher inductive types introduced by homotopy type theory. Our framework also provides a solid basis for such extensions to be built on.