A Formalization of Abstract Rewriting in Agda

TL;DR

This paper provides a constructive formalization of Abstract Rewriting Systems in Agda, clarifying classical concepts, removing classical logic reliance, and applying the framework to lambda calculus.

Contribution

It introduces a constructive Agda formalization of ARS, refines classical criteria, and explores logical relationships between termination notions.

Findings

Refined criteria for termination and confluence.

Eliminated classical logic in proofs.

Applied formalization to lambda calculus.

Abstract

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.