A Formalization of Abstract Rewriting in Agda
This work provides a constructive formalization for proof assistants, addressing foundational issues in term rewriting but is incremental in nature.
The authors formalized Abstract Rewriting Systems in Agda to analyze termination and confluence, refining classical criteria and generalizing results, with an example applied to the lambda calculus.
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.