Templates in Rewriting Induction

1. Problem Statement

The paper addresses a critical bottleneck in Rewriting Induction (RI), a formal system used to prove program equivalence (inductive theorems) in Term Rewriting Systems (TRS). While RI is powerful, its practical application to real-world code often fails due to the difficulty of automatic lemma generation.

• The Divergence Problem: When proving the equivalence of two programs (e.g., different implementations of a factorial function), the proof process often encounters a sequence of equations that do not match. Standard RI techniques (case analysis and rewriting) generate new equations but cannot use previous ones as induction hypotheses because the terms diverge structurally.
• Limitations of Existing Methods:
  • Constraint-based methods (e.g., [9, 12]): These methods attempt to discover loop invariants (e.g., $z = a \times j$) to generalize equations. While effective for simple arithmetic, they fail when the relationship between variables is non-polynomial or when the loop structure is complex.
  • Low-level focus: Existing methods operate at the level of specific variable values and constraints rather than recognizing high-level programming constructs (like tail recursion vs. general recursion).
• Context: The authors focus on Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs), which model real programming code with primitive data types (integers, booleans) and logical constraints (guards), making them more suitable for program verification than standard TRS.

2. Methodology

The authors propose a Template-Based Lemma Generation approach that integrates high-level programming patterns into the Bounded RI proof system.

A. The Concept of Templates

Instead of searching for specific arithmetic invariants, the authors define Templates: rewrite schemes that capture common programming constructs (e.g., upward/downward tail recursion, general recursion).

• Four Core Templates:
  1. TailUp ($T^+$): Upward tail recursion (index increases).
  2. TailDown ($T^-$): Downward tail recursion (index decreases).
  3. RecUp ($R^+$): Upward general recursion.
  4. RecDown ($R^-$): Downward general recursion.
• Higher-Order Recursors: These templates are formalized as higher-order recursors (e.g., tailup, recdn). A specific program is matched to a template by identifying a context function $F$ (the operation performed in the loop) and bounds ($l, u$).

B. The Proof Strategy

The methodology relies on a two-step proof process within Bounded RI:

1. Template-Recursor Equivalence: Prove that a concrete program implementation is equivalent to its corresponding higher-order recursor (e.g., facTU $\approx$ tailup). This is done by structural induction on the loop index.
2. Recursor Equivalence: Prove equivalences between the abstract recursors themselves (e.g., tailup $\approx$ recdn).
   • One-sided Matching: Transform one side of the goal equation into a recursor, then apply a known recursor equivalence to simplify the other side.
   • Two-sided Matching: Transform both sides into their respective recursors and apply a general equivalence theorem directly.

C. Conditional Equivalences

For cases where simple equivalence does not hold (e.g., tailup vs. taildn), the authors introduce Conditional Bounded Inductive Theorems. These proofs rely on axioms (e.g., commutativity and associativity of the operation $F$) and specific ordering requirements to ensure termination and correctness.

3. Key Contributions

1. New Lemma Generation Heuristic: The paper introduces a method that generalizes over loop structures rather than specific variable values. This allows proving equivalences that were previously out of reach for constraint-based invariant generators.
2. Integration with LCSTRS: The approach is specifically designed for Logically Constrained Simply-typed Term Rewriting Systems, allowing for the direct modeling of integer arithmetic and boolean guards without complex encodings.
3. Higher-Order Abstraction: By utilizing higher-order recursors, the system can handle arbitrary operations (like multiplication in factorial or function application in higher-order examples) as parameters, making the templates reusable across different domains.
4. Formal Proof System: The authors define the specific deduction rules (Simplify, Case, Delete, Induct, Hypothesis) and ordering requirements necessary to integrate these templates into the Bounded RI framework.
5. Demonstration of Power: The paper successfully proves equivalences between various factorial implementations (Upward vs. Downward, Tail vs. Recursive) and higher-order variants, including cases where the required invariants are non-polynomial.

4. Results

• Success on Factorial Implementations: The system successfully proved the equivalence of four different factorial implementations (Iterative Up/Down, Recursive Up/Down) under the constraint $x \ge 1$.
  • Key Achievement: Proving facTU $\approx$ facTD (Tail Up vs. Tail Down) was impossible for previous methods ([9, 12]) because the necessary invariants were not polynomial. The template approach solved this by recognizing the structural similarity of the loops.
• Higher-Order Extensions: The method was extended to higher-order functions (e.g., funfacTU), proving equivalence between implementations that apply a function $h$ to the loop index before multiplication.
• Conditional Proofs: The system handled cases requiring axioms (associativity/commutativity) to prove equivalences between different recursion directions (e.g., tailup $\approx$ taildn if the operation is commutative).

5. Significance

• Bridging the Gap: This work bridges the gap between low-level automated theorem proving (which struggles with complex loops) and high-level program verification. It shifts the focus from "finding the right invariant" to "recognizing the right pattern."
• Scalability: By abstracting away specific arithmetic values, the method scales to more complex computational behaviors where polynomial invariants fail.
• Automation Potential: While currently implemented as a manual/semi-automatic process in the tool Cora, the authors argue that template recognition is largely syntactic, suggesting high potential for full automation in future tools.
• Foundational for Program Verification: The approach provides a robust framework for verifying program transformations (e.g., optimizing a recursive function into a tail-recursive one) in the presence of logical constraints, which is essential for verifying modern software systems.

In summary, Hagens and Kop present a paradigm shift in Rewriting Induction: moving from invariant discovery to structural pattern matching, enabling the verification of program equivalences that were previously unprovable due to the complexity of their inductive invariants.