Associativity and Commutativity in Equality Saturation
summary
Extends relational e-matching to handle associative‑commutative operators by storing AC arguments as multisets and adapting tries with a try‑cursor that removes and restores multiset keys; introduces ephemeral e‑class IDs during matching and reuses hash‑consing for roots. Uses leapfrog/generic‑join matching and Kapoor-style AC congruence‑closure. Preliminary results show asymptotically less memory for many cases (multiplying A ten times is essentially free) but matching is incomplete and certain homomorphism patterns cause full subterm materialization and worse memory than traditional e‑graphs.
AI-written summary · about
chapters (8)
- 0:00Associativity and commutativity intro
- 1:51Pattern matching in e-graphs
- 5:17Multi-set for AC operators
- 8:28Ephemeral e-class IDs
- 9:10Congruence closure
- 12:39Memory savings and limits
- 15:29Future work and challenges
- 16:21Q&A
related talks
20mEquality Saturation and Joins
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
19mTowards Relational Contextual Equality Saturation
17mBetter Together: Unifying Datalog and Equality Saturation
24mIncremental Equality Saturation
30megg: Fast and Extensible Equality Saturation
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting
14mAdequacy for Algebraic Effects Revisited