From Rewrite Rules to Axioms in the $λ$$Π$-Calculus Modulo Theory

TL;DR

It is shown that it is possible to replace the rewrite rules of a theory of the $\lambda$$\Pi$-calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof, while maintaining the same expressiveness.

Abstract

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.

Figures (2)

• Figure 1: Typing rules of the $\lambda \Pi$-calculus modulo theory
• Figure 2: Convertibility rules of the $\lambda \Pi$-calculus modulo theory

Theorems & Definitions (2)

• lemma thmcounterlemma: Substitution
• proof