A Formalization of Abstract Rewriting in Agda

This paper presents a constructive formalization of Abstract Rewriting Systems in Agda that eliminates classical logic from standard proofs, refines termination and confluence criteria, and demonstrates its applicability through a formalization of the lambda calculus.

The Gist

Imagine you are a detective trying to solve a mystery in a chaotic city called Rewriting Land. In this city, everything is constantly changing. A shape can transform into another shape, a word can turn into a different word, or a mathematical expression can simplify into a new one.

The rules of this city are called Abstract Rewriting Systems (ARS). The big questions the detectives ask are:

1. Will the chaos ever stop? (Termination): If I keep applying the rules, will I eventually reach a "final form" that can't change anymore, or will I get stuck in an infinite loop forever?
2. Does the path matter? (Confluence): If two different detectives start with the same object and take different paths of changes, will they eventually meet up at the same final destination? Or will they end up at two different, incompatible places?

The Mission: Building a Perfect Map

The authors of this paper, Samuel and Andrew, decided to build a perfect, unbreakable map of this city using a special tool called Agda.

Think of Agda not just as a map, but as a magical construction kit where every proof you build is also a working robot. If you prove that "all paths lead to the same place," the map doesn't just say "Yes"; it actually builds a robot that can take any two different paths and physically merge them into one.

However, there's a catch. Most existing maps of Rewriting Land were drawn using Classical Logic. This is like a map that says, "Either the treasure is here, or it isn't," without actually showing you where it is. It relies on guessing or assuming things exist just because they could exist.

The authors wanted to draw a Constructive Map. This means:

• No guessing.
• No "it must be true because it's not false."
• Every step must be a real, physical action you can perform.
• If you claim a path leads to a treasure, you must be able to walk that path and show the treasure.

The Big Challenges They Solved

1. The "Infinite Loop" Problem (Termination)

In the old maps, proving that a process stops (Strong Normalization) was often done by saying, "If it didn't stop, we'd have a contradiction."
The authors realized that in the real world of computer code, you can't just say "it's a contradiction." You need to actually show the process stopping.

• The Analogy: Imagine a game of "Musical Chairs."
  • Old Map: "If the music never stops, someone must be sitting in a chair that doesn't exist. Therefore, the music must stop." (This is a logical trick).
  • New Map: "We have a specific rule: Every time you move, you must move to a chair that is 'smaller' than the last one. Since you can't have an infinite number of smaller chairs, you must eventually run out of chairs and stop."
  • The Result: They found that for most real-world computer programs (like the ones used in programming languages), this "smaller chair" rule works perfectly without needing any magical guessing.

2. The "Which Path?" Problem (Confluence)

They looked at Newman's Lemma, a famous rule that says: "If the game always stops, and you can always merge two short steps, then you can merge any long path."

• The Twist: The authors found a way to make this rule even stronger. They realized you don't need the game to stop everywhere to guarantee a merge. You just need a specific, slightly weaker condition called "Strongly Minimalizing."
• The Analogy: Imagine two hikers starting at the same mountain peak.
  • Old Rule: "If the mountain is small enough that you can't walk forever, and you can always meet up after one step, you'll meet at the bottom."
  • New Rule: "Even if the mountain is huge, as long as the hikers are following a specific 'downhill' logic where they can't get stuck in a local valley, they will still meet at the bottom."
  • Why it matters: This allows them to prove things about complex systems that the old rules said were too messy to handle.

3. The "Quotient" Problem (Making Sense of Equality)

Sometimes, in math, we want to treat two different things as "the same" (like saying $2+2$is the same as$4$). In computer science, creating a "group" of things that are all equal is hard to do without breaking the rules of the language.

• The Analogy: Imagine you have a pile of clay sculptures. Some look different but are made of the same "recipe." You want to treat them all as one single "Ideal Sculpture."
• The Solution: Instead of trying to glue them all together (which is messy), the authors showed that if your rules for changing the clay are perfect (they stop and they all lead to the same shape), you can just pick the final, unchangeable shape (the Normal Form) to represent the whole group.
• The Benefit: This makes it easy for computers to check if two things are equal. You just run them both until they stop, and if the final shapes look the same, the original things were equal.

Why This Matters to You

You might think, "I'm not a mathematician, why should I care?"

Think about the software you use every day:

• Compilers: The programs that turn your code into an app. They use rewriting rules to simplify your code.
• Type Checkers: The tools that tell you if your code has errors before you run it.
• AI: Large language models often use logic and rewriting to reason.

This paper is like upgrading the engine of these tools. By making the rules of the game "constructive" (real and executable), the authors have:

1. Made proofs into programs: The math they did isn't just a theory; it's code that can actually run and solve problems.
2. Removed the magic: They stripped away the "guessing" parts of the math, making the systems more reliable and predictable.
3. Built a foundation: They created a library of tools that other developers can use to build safer, more powerful programming languages and verification tools.

The Bottom Line

The authors took a messy, chaotic city of changing rules and built a perfect, self-driving guide for it. They showed that you don't need magic or guessing to navigate it; you just need clear, step-by-step instructions that actually work. This makes the software we rely on today more robust, predictable, and easier to verify.

Technical Summary

Here is a detailed technical summary of the paper "A Formalization of Abstract Rewriting in Agda" by Samuel Arkle and Andrew Polonsky.

1. Problem Statement

The paper addresses the challenge of formalizing Abstract Rewriting Systems (ARS) within a constructive framework (specifically using the Agda proof assistant).

• The Conflict: Standard presentations of ARS theory (e.g., in the textbook Terese by Bezem, Klop, and De Vrijer) rely heavily on classical logic (e.g., the Law of Excluded Middle, proof by contradiction).
• The Goal: The authors aim to create a library where proofs are not just verifications of validity but effective programs (adhering to the Curry-Howard isomorphism). This requires eliminating classical axioms where possible and making decidability hypotheses explicit.
• The Motivation: A constructive ARS library is essential infrastructure for formalizing programming language theory (PLT). It enables:
  • Computational extraction: Proofs of confluence automatically yield algorithms to compute common reducts.
  • Quotient construction: In type theory, constructing quotients (e.g., for initial models of algebraic theories) is difficult. If a system is confluent and terminating, the quotient can be represented effectively by the type of normal forms, avoiding complex extensions like Higher Inductive Types.

2. Methodology

The authors developed a formalization in Agda based on Martin-Löf Intuitionistic Type Theory, adhering to strict constructive principles:

• No Classical Axioms: They avoided axioms such as Function Extensionality, Univalence, Uniqueness of Identity Proofs (UIP), and Axiom K.
• Explicit Decidability: Where classical logic was historically used, they replaced it with explicit decidability hypotheses (e.g., $Rxy \lor \neg Rxy$).
• Refinement of Definitions: They re-examined standard definitions (like Strong Normalization and Well-foundedness) to identify which variations are constructively equivalent and which require classical assumptions.
• Code-First Approach: The paper structure mirrors the Agda codebase. Theoretical results are stated with references to specific Agda functions rather than traditional mathematical proofs, emphasizing that the code is the proof.

3. Key Contributions

A. Taxonomy of Termination and Confluence

The authors constructed a detailed hierarchy of ARS properties, analyzing the logical implications between them in a constructive setting.

• New Concepts: They introduced and formalized new properties to bridge gaps in the constructive hierarchy:
  • Minimal Forms (MF): Elements that cannot be reduced further in a specific sense.
  • Strongly/Weakly Minimalizing (SM/WM): Properties related to reaching minimal forms.
  • Recurrence Property (RP): A replacement for the "Increasing" property (Inc) found in standard texts, which is computationally expensive to satisfy.
• Hierarchy Analysis: They mapped out implications between properties like Strong Normalization (SN), Weak Normalization (WN), Church-Rosser (CR), and Weak Church-Rosser (WCR).
  • Key Finding: The implication $SN \implies WN$ is not constructively provable in general. It requires the relation to be decidable and finitely branching.
  • Key Finding: $WN \land UN_{\to} \implies CR$ holds constructively without classical assumptions, whereas $SN \land UN_{\to} \implies CR$ does not.

B. Generalization of Newman's Lemma

• Classical Result: Newman's Lemma states that $SN \land WCR \implies CR$.
• Constructive Generalization: The authors proved a generalized version: $SM \land WCR \implies CR$.
  • Here, $SM$ (Strongly Minimalizing) is a weaker condition than $SN$. This allows the lemma to apply to systems that are not strongly normalizing (e.g., systems with infinite reductions that still possess a "perpetual" reduction strategy) but are still confluent.

C. Analysis of Well-Foundedness

The paper provides a rigorous comparison of various definitions of well-foundedness, which are classically equivalent but distinct constructively:

1. Accessible (WFacc): Inductive definition (standard for SN).
2. Inductive (WFind): Every inductive predicate holds.
3. Coreductive (WFcor): Every coreductive predicate holds.
4. Minimality (WFmin): Every non-empty subset has a minimal element.
5. Sequential (WFseq): No infinite decreasing sequences exist.

Key Insights on Well-Foundedness:

• Only $WFacc$ and $WFind$ are constructively equivalent.
• $WFmin$ (existence of minimal elements) is a very strong assumption; asserting it for natural numbers implies the decidability of all subsets of $\mathbb{N}$, which is incompatible with constructive semantics.
• The authors identified specific classical principles (e.g., $accDNE$, $accCor$) required to bridge these definitions. They showed that for finitely branching and decidable relations (common in Term Rewriting Systems), the necessary classical principles hold, making the results effective.

D. Application to Lambda Calculus

The library was applied to the untyped lambda calculus using a nested type encoding (functorial representation).

• Results: The library successfully derived standard results (confluence, decidability of normal forms) as consequences of the general ARS theory.
• Significance: This demonstrated that the heterogeneous nature of lambda terms (where types depend on other types) does not interfere with the general ARS formalization, validating the library's reusability.

4. Results

• Effectiveness: Most standard ARS results can be made completely effective for practical systems (first-order TRS and lambda calculi) by assuming decidability and finite branching.
• Optimization: The authors refined standard criteria, showing that some classical assumptions are stronger than necessary. For instance, replacing the "Increasing" property with the "Recurrence" property ($RP$) allows for broader applicability.
• Counterexamples: The formalization identified specific counterexamples (e.g., Counter-example 4 in the paper) where global properties do not imply local ones, or where classical implications fail without decidability.
• Logical Dependencies: A comprehensive diagram (Figure 2 in the paper) was produced showing exactly which classical axioms are needed to transition between different definitions of well-foundedness.

5. Significance

• Infrastructure for PL Theory: This work "bootstraps" a formalized programming language theory repository at Appalachian State University. It provides a verified, executable foundation for proving properties of complex languages.
• Constructive Clarity: By stripping away classical logic, the authors revealed hidden dependencies on decidability. This clarifies when and why certain rewriting properties hold, distinguishing between systems that are merely "true" in classical logic and those that are "computable."
• Algorithmic Extraction: Because the proofs are constructive, they serve as executable algorithms. For example, a proof of confluence in Agda can be extracted to a function that computes the common reduct of two terms.
• Future Work: The authors suggest using this library to import termination certificates from external automated provers (like those from the Termination Competition) into Agda, bridging the gap between automated verification and interactive theorem proving.

In summary, the paper successfully transforms Abstract Rewriting from a classical mathematical theory into a constructive, computational framework, identifying the precise logical boundaries where classical assumptions are necessary and providing a robust library for future formalizations in computer science.