构造演算中由重写定义的概念

本文提出一组一般语法条件，确保构造代数演算（Calculus of Algebraic Constructions）的强归正性和逻辑一致性。该演算是构造演算（Calculus of Constructions）的一种扩展，引入了由高阶重写规则定义的函数和谓词。一方面，构造演算是一种强大的类型系统，可用于形式化高阶逻辑的命题和自然演绎证明；另一方面，重写是一种简单且功能强大的计算范式。两者的结合使得可以develop（开发）形式证明，相较于更传统的证明助手，具有更小的规模和更自动化的特征。主要创新点在于考虑一种一般形式的谓词级重写，这种重写是构造演算中归纳构造（Calculus of Inductive Constructions）强消除（strong elimination）的通用化。