Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
summary
E-graphs gain native support for bound variables by making e-classes functions over parameterized e-classes (slots) so alpha-equivalent terms share a single representation; this avoids de Bruijn index shifting and the copy explosion. Implementation integrates with egg-style rewriting and is evaluated on a synthetic family (increasing function arity), SDQL compiler benchmarks, and a Lean tactic backend. Results show fewer iterations, much smaller e-graphs in many cases (sometimes up to 50x memory), shorter proofs, and an instance solved in ~1s where the de Bruijn baseline times out.
AI-written summary · about
chapters (11)
- 0:00Slotted E-graphs intro
- 2:13Bound variables problem
- 5:26Slotted E-graphs concept
- 8:13Handling binders
- 10:38Parameterized equivalence classes
- 11:41Rice array language case
- 13:03Revert problems performance
- 13:44SDQL optimization results
- 15:26Lean tactic outcomes
- 16:08Paper and implementation
- 16:29Q&A
related talks
23mSlotted E-Graphs
23mVersioned E-Graphs
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
23mPerformant Dynamically Typed E-Graphs in Pure Julia
25mLifting E-Graphs: A Function Isn’t a Constant
22mFrom Rewriting to Fixpoints: Solving Recursive Equations with E-Graphs
25mDisequalities in E-Graphs: An Experiment