From Rewrite Rules to Axioms in the $λ$$Π$-Calculus Modulo Theory
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909106209554432 |
|---|---|
| author | Blot, Valentin Dowek, Gilles Traversié, Thomas Winterhalter, Théo |
| author_facet | Blot, Valentin Dowek, Gilles Traversié, Thomas Winterhalter, Théo |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_09024 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | From Rewrite Rules to Axioms in the $λ$$Π$-Calculus Modulo Theory Blot, Valentin Dowek, Gilles Traversié, Thomas Winterhalter, Théo Logic in Computer Science 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. |
| title | From Rewrite Rules to Axioms in the $λ$$Π$-Calculus Modulo Theory |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2402.09024 |