关于非直谓纯类型系统一致性的机器检查证明
A Machine-checked Proof of Consistency for Impredicative Pure Type Systems
中文总结 AI 辅助
研究非直谓纯类型系统的一致性，通过使用经典语法和多重替换，给出β归约合流性、主体归约及一致性证明，发展α交换关系理论，用Agda机器检查，取得类型理论机械化方法的进展。
中文摘要 AI 辅助
本文继续评估使用经典语法和斯托顿多重替换来实现类型理论机械化方法的可行性，并报告了一些重大进展。我们给出了β归约合流性的形式证明，通过高桥对泰特和马丁-洛夫证明的修正，给出了纯类型系统族的主体归约以及一些非直谓子类在假设规范化下的一致性证明。对于合流性证明，我们还发展了α交换关系理论。最后评估了该方法的优缺点。整个开发使用Agda进行了机器检查。
英文摘要
In this paper we continue assessing the feasibility of the approach to the mechanization of type theory by using classical syntax and Stoughton's multiple substitutions and report some substantial progress. We present formal proofs of confluence for beta-reduction and by using Takahashi's revision of Tait and Martin-Löf's proof, subject reduction for the entire family of the Pure Type Systems and consistency for some impredicative subclass, assuming normalization. As to the proof of confluence, we also develop a theory of alpha-commutative relations which, in our view, entails a clearer presentation and treatment of the problem than in similar developments. Finally, we assess general merits and drawbacks of the approach. The whole development has been machine-checked using Agda.
