From Rewriting to Fixpoints: Solving Recursive Equations with E-Graphs
summary
Extends e-graphs to represent recursive variables by adding secondary definitional edges that link a variable to its definition without merging, builds a transition system from e-classes, and uses bisimulation to extract fixed‑point equations whose coincidence lets e-classes merge. Prototype shows rewrites plus simulation can prove equalities but breaks on unsound merges (unproductive cycles) and non‑unique solutions. Remedies include variable‑generic equalities to restrict rewrites and productivity tracking (guarded unfoldings); work remains fragile—counterexamples force more iteration‑theory checks.
AI-written summary · about
chapters (9)
- 0:00Welcome
- 0:50Motivation for fixed points
- 3:43Solution coincidence intuition
- 5:33Saturating egraphs
- 10:10Soundness and productivity challenges
- 14:45Tracking productivity in cycles
- 15:28Non-unique solutions
- 17:20Summary
- 17:45Q&A
related talks
38mE-graphs and Automated Reasoning: Looking back to look forward
19mDestructive E-Graph Rewrites
23mVersioned E-Graphs
20mSlotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
22mAutomated Proof Generation for Associative and Distributive Rewriting with E-Graphs
24mOptimism in Equality Saturation
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs