From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory
CoRR(2024)
摘要
The λΠ-calculus modulo theory is an extension of simply typed
λ-calculus with dependent types and user-defined rewrite rules. We show
that it is possible to replace the rewrite rules of a theory of the
λΠ-calculus modulo theory by equational axioms, when this theory
features the notions of proposition and proof, while maintaining the same
expressiveness. To do so, we introduce in the target theory a heterogeneous
equality, and we build a translation that replaces each use of the conversion
rule by the insertion of a transport. At the end, the theory with rewrite rules
is a conservative extension of the theory with axioms.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要