Lifting E-Graphs: A Function Isn’t a Constant
summary
Proposes encoding α-equivalence by baking thinning bit vectors into e-nodes so terms carry their context; implements fat identifiers (ID plus thinning) and a thinning union-find that composes thinnings on find and peels common lifts on union. Demonstrates lift-pulling smart constructors that recover sharing lost by naive naming, shows E-matching composes thinnings down tree, gives tiny Python combinators for lift composition, and notes permutations are more general but thinnings are simpler and enough for many practical cases.
AI-written summary · about
chapters (14)
- 0:00Lifting e-graphs introduction
- 1:26Named variables problems
- 3:53Semantic meaning of sin(x)
- 5:17Nameless dimensions
- 8:26No sharing between functions
- 9:08Introducing lifting and thinnings
- 10:53Why thinnings are powerful
- 13:37Baking lifting into e-graphs
- 16:45Lift pulling smart constructors
- 17:49Thinning union-find explained
- 19:33Semantics of unioning thinned IDs
- 20:55E-matching with thinnings
- 23:01Related work and connections
- 24:27Q&A on thinning vs permutations
related talks
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
23mSlotted E-Graphs
23mVersioned E-Graphs
20mSlotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
38mE-graphs and Automated Reasoning: Looking back to look forward
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
25mDisequalities in E-Graphs: An Experiment
23mPerformant Dynamically Typed E-Graphs in Pure Julia