Introduction

Every optimizing compiler faces an awkward dilemma: which rewrites to apply, and in what order? Replacing a×2a \times 2 with a≪1a \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.

Saturate and Extract

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).

<!-- E-graph equality saturation demo -->
<p class="hint">Start with <code>(2*a)*(a/1)</code> — cost 7 operators. Fire rewrite rules to grow the equivalence set, then extract the cheapest form.</p>
<div class="expr-row">
  <span class="label">Expression:</span>
  <code id="current-expr" class="expr-display"></code>
</div>
<div class="equiv-box" id="equiv-box">
  <div class="box-title">Equivalent forms found so far</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">Saturate step</button>
  <button id="btn-saturate" type="button">Saturate all</button>
  <button id="btn-extract" type="button">Extract cheapest</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>
<div class="extracted-row" id="extracted-row" style="display:none">
  <span class="label">Best form:</span>
  <code id="extracted-expr" class="expr-display best"></code>
  <span id="extracted-cost" class="cost-badge"></span>
</div>

/* Styles for the equality saturation demo */
* { 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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Equality saturation demo — BFS over equivalent expressions
// We generate all equivalent full expressions via BFS; each step fires all rules at every sub-tree position.

// Cost = total AST node count (operators + leaves)
function cost(n){
  if(!n.args||n.args.length===0) return 1;
  return 1 + n.args.reduce(function(s,c){ return s+cost(c); }, 0);
}
function exprStr(n){
  if(n.op==='num') return String(n.val);
  if(n.op==='var') return n.name;
  if(n.op==='sq')  return 'sq('+exprStr(n.args[0])+')';
  if(n.op==='<<')  return exprStr(n.args[0])+'<<'+exprStr(n.args[1]);
  return '('+exprStr(n.args[0])+n.op+exprStr(n.args[1])+')';
}
function exprEq(a,b){
  if(a.op!==b.op) return false;
  if(a.op==='num') return a.val===b.val;
  if(a.op==='var') return a.name===b.name;
  if(!a.args||!b.args||a.args.length!==b.args.length) return false;
  return a.args.every(function(x,i){ return exprEq(x,b.args[i]); });
}
function exprKey(n){ return exprStr(n); }

// Rewrite rules: produce all one-step variants of an expression
// Rules: x/1->x, 2*x->x<<1, commutativity, x*x->sq(x)
function oneStepVariants(expr){
  var result = [];
  // rule: x / 1 -> x
  if(expr.op==='/'&&expr.args&&exprEq(expr.args[1],{op:'num',val:1}))
    result.push(expr.args[0]);
  if(expr.op==='*'&&expr.args){
    // rule: 2*x -> x<<1 (strength reduction)
    if(exprEq(expr.args[0],{op:'num',val:2}))
      result.push({op:'<<',args:[expr.args[1],{op:'num',val:1}]});
    if(exprEq(expr.args[1],{op:'num',val:2}))
      result.push({op:'<<',args:[expr.args[0],{op:'num',val:1}]});
    // rule: a*b -> b*a (commutativity)
    result.push({op:'*',args:[expr.args[1],expr.args[0]]});
    // rule: x*x -> sq(x) (squaring)
    if(exprEq(expr.args[0],expr.args[1]))
      result.push({op:'sq',args:[expr.args[0]]});
  }
  // apply rules recursively in sub-expressions and rebuild parent
  if(expr.args){
    for(var i=0;i<expr.args.length;i++){
      var childVars = oneStepVariants(expr.args[i]);
      for(var j=0;j<childVars.length;j++){
        var newArgs=expr.args.slice(); newArgs[i]=childVars[j];
        result.push({op:expr.op,args:newArgs});
      }
    }
  }
  return result;
}

// Initial expression: (2 * a) * (a / 1)  cost = 7
var INITIAL_EXPR = { op: '*', args: [
  { op: '*', args: [{ op: 'num', val: 2 }, { op: 'var', name: 'a' }] },
  { op: '/', args: [{ op: 'var', name: 'a' }, { op: 'num', val: 1 }] }
]};

// State: all known equivalent forms + BFS frontier
var equivMap = new Map();  // key -> expression object for all known equivalents
var frontier = [];         // expressions added in the last step (BFS frontier)
var saturated = false;
var stepCount = 0;
var lastNewKeys = [];

function init(){
  equivMap = new Map();
  frontier = [INITIAL_EXPR];
  equivMap.set(exprKey(INITIAL_EXPR), INITIAL_EXPR);
  saturated = false;
  stepCount = 0;
  lastNewKeys = [exprKey(INITIAL_EXPR)];
}

// One saturation step: expand each frontier expression by one rule application
function doStep(){
  if(saturated||frontier.length===0) return false;
  var nextFrontier = [];
  lastNewKeys = [];
  for(var fi=0;fi<frontier.length;fi++){
    var variants = oneStepVariants(frontier[fi]);
    for(var vi=0;vi<variants.length;vi++){
      var k = exprKey(variants[vi]);
      if(!equivMap.has(k)){
        equivMap.set(k, variants[vi]);
        nextFrontier.push(variants[vi]);
        lastNewKeys.push(k);
      }
    }
  }
  frontier = nextFrontier;
  if(frontier.length===0) saturated=true;
  return lastNewKeys.length>0;
}

// Extract: find the minimum-cost expression across all equivalents
function extractBest(){
  var best=null, bestCost=Infinity;
  equivMap.forEach(function(expr){
    var c=cost(expr);
    if(c<bestCost){ bestCost=c; best=expr; }
  });
  return {expr:best, cost:bestCost};
}

function renderEquiv(highlightBest){
  var cont=document.getElementById('equiv-container');
  cont.innerHTML='';
  var bestKey=null;
  if(highlightBest){
    var b=extractBest(); if(b.expr) bestKey=exprKey(b.expr);
  }
  equivMap.forEach(function(expr,k){
    var chip=document.createElement('span');
    var isNew=lastNewKeys.indexOf(k)>=0;
    var isBest=highlightBest&&k===bestKey;
    chip.className='equiv-chip'+(isNew?' new':'')+(isBest?' best-chip':'');
    chip.textContent=exprStr(expr);
    cont.appendChild(chip);
  });
}
function setStatus(msg,cls){
  var s=document.getElementById('status-row');
  s.textContent=msg; s.className='status-row '+(cls||'');
}

function reset(){
  init();
  document.getElementById('current-expr').textContent=exprStr(INITIAL_EXPR);
  document.getElementById('extracted-row').style.display='none';
  setStatus('Ready. Press ’Saturate step’ to fire rewrite rules.','info');
  renderEquiv(false);
  document.getElementById('btn-step').disabled=false;
  document.getElementById('btn-saturate').disabled=false;
}

document.getElementById('btn-step').addEventListener('click',function(){
  if(saturated){ setStatus('Already saturated — no new equivalences possible.','done'); return; }
  stepCount++;
  doStep();
  renderEquiv(false);
  if(saturated) setStatus('Saturated! All equivalent forms found.','done');
  else setStatus(fmt('Step %stepCount% — %size% equivalent forms so far.', { stepCount: stepCount, size: equivMap.size }),'ok');
});

document.getElementById('btn-saturate').addEventListener('click',function(){
  if(saturated){ setStatus('Already saturated — no new equivalences possible.','done'); return; }
  while(!saturated&&stepCount<20){ stepCount++; doStep(); }
  renderEquiv(false);
  setStatus(fmt('Saturated! Found %size% equivalent forms. Now extract the cheapest.', { size: equivMap.size }),'done');
});

document.getElementById('btn-extract').addEventListener('click',function(){
  var result=extractBest();
  if(!result.expr){ setStatus('No expressions yet — reset first.',''); return; }
  document.getElementById('extracted-expr').textContent=exprStr(result.expr);
  document.getElementById('extracted-cost').textContent=fmt('cost %cost%', { cost: result.cost });
  document.getElementById('extracted-row').style.display='flex';
  renderEquiv(true);
  setStatus(fmt('Extracted cheapest form: cost %cost% (original was %cost2%). Highlighted in orange.', { cost: result.cost, cost2: cost(INITIAL_EXPR) }),'ok');
});

document.getElementById('btn-reset').addEventListener('click', reset);

reset();
Result
Console

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.

The Real Complexity

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→xx + 0 \to x, but also x→x+0x \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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/e-graphs/Content licensed under CC BY-NC 4.0.