E-graphs & Equality Saturation

Every optimizing compiler faces an awkward dilemma: which rewrites to apply, and in what order? Replacing $a \times 2$ with $a \ll 1$ (a left bit-shift) might unlock a later simplification — or might block one. Apply too few rewrites and leave performance on the table; chase the wrong sequence and miss the global optimum.

The traditional answer is to pick a fixed order, accept the losses, and move on. But since 2005, and especially since the egg library (Willsey et al., POPL 2021) made it practical, a richer answer has emerged: equality saturation.

The key ingredient is the e-graph (equality graph). An e-graph groups expressions into e-classes — sets of provably equivalent terms — and represents the whole group at once rather than committing to a single form. When you apply a rewrite rule the graph simply grows: both the old and new form exist, linked in the same equivalence class. Apply all your rules exhaustively and the e-graph reaches saturation: every expression equivalent to the original lives inside it. Then a single extraction pass walks the graph and picks out the cheapest variant — and the order in which rewrites fired never mattered.

The result is a clean separation: equality (what is true) and cost (what is cheap) are handled in two completely independent phases.

Below is a small arithmetic expression. The engine knows a handful of rewrite rules — algebraic identities and strength-reduction tricks. Each Saturate step fires all applicable rules and grows the e-graph. When no new equivalences can be added the graph is saturated. Then Extract cheapest walks every e-class and picks the form with the lowest cost (operator count).

<!-- {{c_html_intro}} -->
<p class="hint">{{hint_para}}</p>
<div class="expr-row">
  <span class="label">{{label_expr}}</span>
  <code id="current-expr" class="expr-display"></code>
</div>
<div class="equiv-box" id="equiv-box">
  <div class="box-title">{{label_equiv}}</div>
  <div id="equiv-container" class="equiv-container"></div>
</div>
<div class="status-row" id="status-row"></div>
<div class="btns">
  <button id="btn-step" type="button">{{btn_step}}</button>
  <button id="btn-saturate" type="button">{{btn_saturate}}</button>
  <button id="btn-extract" type="button">{{btn_extract}}</button>
  <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
</div>
<div class="extracted-row" id="extracted-row" style="display:none">
  <span class="label">{{label_best}}</span>
  <code id="extracted-expr" class="expr-display best"></code>
  <span id="extracted-cost" class="cost-badge"></span>
</div>

/* {{c_css_intro}} */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .8rem; line-height: 1.5; }
.expr-row { display: flex; align-items: center; gap: .5rem; margin-bottom: .6rem; flex-wrap: wrap; }
.label { font-size: .8rem; color: #666; font-weight: 600; white-space: nowrap; }
.expr-display { background: #e8eef3; border: 1px solid #cdd9e3; border-radius: 6px;
                padding: .25rem .55rem; font-size: .92rem; color: #1d3557; }
.expr-display.best { background: #d4edda; border-color: #a8d5b5; color: #155724; }
.equiv-box { border: 1.5px solid #cdd9e3; border-radius: 10px; padding: .6rem .8rem;
             background: #f7fafc; margin-bottom: .65rem; min-height: 60px; }
.box-title { font-size: .72rem; font-weight: 700; color: #5a7088; text-transform: uppercase;
             letter-spacing: .06em; margin-bottom: .45rem; }
.equiv-container { display: flex; flex-wrap: wrap; gap: .35rem; }
.equiv-chip { border: 1.5px solid #5a7088; border-radius: 6px; padding: .18rem .5rem;
              background: #fff; font-size: .8rem; font-family: ui-monospace, monospace;
              color: #1d3557; white-space: nowrap; }
.equiv-chip.new { border-color: #0a7d33; color: #0a7d33; background: #f0fff4; font-weight: 700; }
.equiv-chip.best-chip { border-color: #856404; color: #856404; background: #fff3cd; }
.status-row { font-size: .88rem; font-weight: 600; min-height: 1.4em; margin: .3rem 0; }
.status-row.ok { color: #0a7d33; }
.status-row.info { color: #1d3557; }
.status-row.done { color: #856404; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .6rem; }
button { font: 600 13px system-ui; padding: .38rem .82rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .45; cursor: default; }
.extracted-row { display: flex; align-items: center; gap: .5rem; flex-wrap: wrap; }
.cost-badge { font-size: .78rem; background: #fff3cd; border: 1px solid #ffc107;
              border-radius: 5px; padding: .15rem .45rem; color: #856404; font-weight: 700; }

// Code not found

Notice that at saturation the e-graph holds all equivalent forms simultaneously. You never had to choose an order for the rewrites — every path was explored. Extraction happens once, at the end, and it always finds the global optimum among the terms the rules can reach.

Equality saturation sounds almost magical — explore everything and then pick the best. So what is the catch?

• Termination is not guaranteed. If the rewrite rules can generate infinitely many distinct terms (e.g., $x + 0 \to x$, but also $x \to x + 0$ in the other direction) the e-graph grows forever and saturation is never reached. Practitioners carefully curate rule sets or set a time/node budget.
• Space can blow up. Even with termination, the number of e-nodes can grow exponentially in the number of rewrites. The egg library uses rebuilding — deferred congruence closure — to keep the cost manageable in practice.
• Extraction is NP-hard in general. Finding the minimum-cost expression across all e-classes is equivalent to an integer linear program. For DAG-shaped costs (where sharing a sub-expression saves work) the problem is NP-hard. For tree costs it reduces to a polynomial per-e-class DP.
• The general question is undecidable. Whether two arbitrary terms are equatable by a given rewrite system is equivalent to the halting problem — no algorithm can always answer it.

Despite these limits, equality saturation is remarkably effective on the bounded, terminating rule sets typical in compilers, and the egg library's design has made it fast enough for production use.

Equality saturation has escaped the theory lab and reached production systems in several domains:

• Compiler backends: the Cranelift code generator (used in Wasmtime and Firefox) replaced ad-hoc peephole passes with an equality-saturation engine. Rule sets are concise and correct-by-construction — a new optimization is just a new rewrite rule.
• Floating-point accuracy: Herbie uses equality saturation to automatically rewrite floating-point expressions into numerically stable equivalents, winning significant accuracy on real scientific benchmarks.
• Tensor graph optimization: Tensat applies equality saturation to deep-learning computation graphs (ONNX, TVM), finding operator fusions and layout transforms that sequential passes miss.
• Program synthesis and verification: equality saturation is closely related to program equivalence checking — if two programs saturate into the same e-class they are provably equivalent.
• Database query optimization: recent work encodes relational algebra rewrites as e-graph rules, letting the optimizer explore join orderings and predicate push-downs simultaneously.

The common thread: whenever many small, local rewrites interact and their best global combination is hard to guess, an e-graph turns the combinatorial search into a compact, reusable structure.

The insight behind e-graphs is conceptually clean: never throw away an equivalent form. Pack every reachable expression into one structure, saturate it with your rules, and only then ask which form is cheapest. The order of rewrites becomes irrelevant, and the phase-ordering problem that haunts traditional compilers simply dissolves.

The practical impact — via egg, Cranelift, Herbie, and Tensat — shows that this is not just theory. Equality saturation is fast enough and expressive enough to replace bespoke optimization passes in real tools. And the connection runs deep: at its heart an e-graph is a compressed representation of an equivalence relation, the same mathematical object that underlies program equivalence and the halting problem. Exploring what it means for two things to be the same turns out to be one of the most powerful tools we have for making programs faster.