构造演算中重写的相容性与完备性

在基于 Curry-Howard 同构的证明助手（如 Coq）中添加重写规则，可极大提升工具的可用性。不幸的是，添加任意一组重写规则可能导致底层形式系统不可判定且不相容。虽然确保终止性和合流性（从而确保类型检查的判定性）的方法已得到一定程度的研究，但逻辑相容性迄今为止鲜少受到关注。本文表明，相容性是典范性（canonicity）的推论，而典范性又源于所有由重写规则定义的函数均为完备的这一假设。我们提供了一个可靠且终止、但必然不完备的算法来验证该性质。该算法接受所有遵循 Coquand 提出的依赖模式匹配方案并由 McBride 在其博士论文中研究的定义。它同时也接受许多通过重写进行的定义，其中包含偏离标准模式匹配的规则。