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

Valentin Blot (1, 2, 3, 4) , Gilles Dowek (1, 2, 3, 4) , Thomas Traversié (1, 5, 2, 3, 4) , Théo Winterhalter (1, 2, 3, 4)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
2 LMF - Laboratoire Méthodes Formelles
3 ENS Paris Saclay - Ecole Normale Supérieure Paris-Saclay
4 Université Paris-Saclay
5 CentraleSupélec

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 axioms of equality, 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. We construct a translation that replaces each use of the conversion rule by the insertion of a transport. To facilitate the proofs, we consider a type system in which conversions are explicitly typed.

Keywords: Rewrite rules; Equality; Logical Framework; Dependent types

Domains: Logic in Computer Science [cs.LO]

Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter. From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory. 2023. ⟨hal-04275229v1⟩