一句话：提出一种用户可扩展的相等性检查算法，适用于一大类依赖类型理论，并在 Andromeda 2 中实现。
本文面向依赖类型理论中相等性判定难以通用且难以由用户扩展的问题，提出一种通用、用户可扩展的相等性检查算法。算法由两个阶段组成：类型导向阶段应用外延性规则，规范化阶段应用计算规则；两类规则均用类型论中的 object-invertible 规则概念定义。作者给出识别此类规则的充分语法条件及简单的模式匹配算法，并引入主参数（principal arguments）概念以确定范式，通过改变主参数可得到弱头范式、强范式等已知概念。文章证明该算法是可靠的（sound），并在支持用户自定义类型理论的证明助手 Andromeda 2 中实现。用户只需提供相等性规则，算法会自动将其分类为计算规则或外延性规则，并选择合适的主参数。
We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on computation rules, where both kinds of rules are defined using the type-theoretic concept of object-invertible rules. We also give sufficient syntactic criteria for recognizing such rules, as well as a simple pattern-matching algorithm for applying them. A third component of the algorithm is a suitable notion of principal arguments, which determines a notion of normal form. By varying these, we obtain known notions, such as weak head-normal and strong normal forms. We prove that our algorithm is sound. We implemented it in the Andromeda 2 proof assistant, which supports user-definable type theories. The user need only provide the equality rules they wish to use, which the algorithm automatically classifies as computation or extensionality rules, and select appropriate principal arguments.
@article{paperbot1743,
title = {An extensible equality checking algorithm for dependent type theories},
author = {Andrej Bauer and Anja Petković Komel},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:17)2022}
}