| Autor: |
Blot, Valentin, Dowek, Gilles, Traversié, Thomas, Winterhalter, Théo |
| Rok vydání: |
2024 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| Popis: |
The $\lambda$$\Pi$-calculus modulo theory is an extension of simply typed $\lambda$-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 $\lambda$$\Pi$-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. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
