EQUALITY SATURATION stop choosing which rewrite first; apply them all
Every other pass in this batch picks an order and commits — strength-reduce first, or cancel first? — and a wrong choice hides the win the other order would have found. This is the phase-ordering problem. Equality saturation refuses to choose: it keeps all equivalent forms at once in an e-graph, applies every rewrite rule until nothing new appears (saturation), then extracts the cheapest form. One structure, every order, at once.
THE TECHNIQUE e-graph + saturate + extract cheapest
Start from (x*2)/2. A greedy pass in the wrong order gets stuck; equality saturation grows the e-graph with every rule (x*2→x<<1, (x*c)/c→x, x*1→x), keeps them all in one class, then extracts x. Compare a single-order pass against saturation: live demo
HISTORY & CREDIT Tate et al. 2009; e-graphs Nelson-Oppen 1980
“E-graphs are a new (egg-era) idea.” — no. The e-graph and its congruence closure are from Nelson & Oppen, 1980, in automated theorem proving. Equality saturation (2009) is what applied them to compiler optimisation; egg (2021) made them fast and reusable. cited
1980 · Greg Nelson & Derek Oppen (and Nelson’s 1980 thesis) — congruence closure and the e-graph, for deciding equalities in theorem provers; contemporaneous with Downey-Sethi-Tarjan’s 1980 congruence-closure work (same JACM volume), not derived from it. 2009 · Ross Tate, Michael Stepp, Zachary Tatlock & Sorin Lerner — “Equality Saturation: A New Approach to Optimization” (POPL): grow an e-graph with rewrites, then extract — the phase-ordering problem dissolved. 2021 · Willsey, Nandi, Wang, Flatt, Tatlock & Panchekha — “egg” (POPL): fast, extensible equality saturation with deferred rebuilding; sparks a wave of real uses.
Extraction (pick the cheapest term from the saturated graph) is itself an optimisation problem — greedy by node cost, or an ILP for the true optimum when sharing matters. Saturation may not terminate, so rules run under a budget. Tate-Stepp-Tatlock-Lerner, 2009
RECOMMEND FOR I-13 every form is equal on the machine
The equalities the e-graph asserts — that (x*2)/2, the shift form, and x are all the same value — hold on the canonical compiler, so extraction to x is sound:
$ i13 run eqsat.i13 # (x*2)/2 , (x<<1)>>1 , x -- all one e-class
x = 21
mul_div = 21 -- (x * 2) / 2
shift = 21 -- (x << 1) >> 1 (strength-reduced form)
ident = 21 -- x (extracted: cheapest, 0 ops)
Recommend: equality saturation is the batch’s capstone and its keeper claim — verified on the canonical compiler that (x*2)/2, the shifted form, and bare x all evaluate to 21, so an e-graph may hold them in one class and extract the zero-op form. Where SSA/SCCP/GVN/copy-prop/inline/PRE each fix an order and can miss what another order would find, equality saturation subsumes the phase-ordering problem the other seven embody: it applies all their rewrites at once and picks the best. On a small, bounded language like I-13 — finite terms, cheap congruence — a bounded e-graph is buildable today (union-find over term-nodes + a rewrite list + min-cost extraction).