A Formalization of Abstract Rewriting in Agda
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912961882226688 |
|---|---|
| author | Arkle, Sam Polonsky, Andrew |
| author_facet | Arkle, Sam Polonsky, Andrew |
| contents | We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to termination and confluence and investigate the relationships between them and their classical counterparts. We identify, and eliminate where possible, the use of classical logic in the proofs of standard ARS results. Our analysis leads to refinements and mild generalizations of classical termination and confluence criteria. We investigate logical relationships between several notions of termination, arising from different formulations of the concept of a well-founded relation. We illustrate general applicability of our ARS development with an example formalization of the lambda calculus. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_10936 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Formalization of Abstract Rewriting in Agda Arkle, Sam Polonsky, Andrew Logic in Computer Science Logic 68Q42 (Primary) 68V15 (Secondary) We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to termination and confluence and investigate the relationships between them and their classical counterparts. We identify, and eliminate where possible, the use of classical logic in the proofs of standard ARS results. Our analysis leads to refinements and mild generalizations of classical termination and confluence criteria. We investigate logical relationships between several notions of termination, arising from different formulations of the concept of a well-founded relation. We illustrate general applicability of our ARS development with an example formalization of the lambda calculus. |
| title | A Formalization of Abstract Rewriting in Agda |
| topic | Logic in Computer Science Logic 68Q42 (Primary) 68V15 (Secondary) |
| url | https://arxiv.org/abs/2603.10936 |