The easiest compiler bug to understand is a wrong rewrite.

The more interesting compiler bug is a right rewrite at the wrong time.

Suppose the optimizer sees:

(a * 2) / 2

Strength reduction says:

a * 2  ->  a << 1

That is locally attractive. Shifts are cheap. So a destructive optimizer can turn the program into:

(a << 1) / 2

But another path was waiting:

(a * 2) / 2
-> a * (2 / 2)
-> a * 1
-> a

Both first steps were valid. One made the expression cheaper immediately. The other preserved the shape needed for cancellation.

This is the phase-ordering problem in miniature. Optimizations are individually reasonable, but the sequence matters. Once a compiler destructively rewrites a program, it may erase the syntactic opportunity that a later optimization needed.

Equality saturation attacks the problem by refusing to choose too early.

Rewrites Become Equations Again

Term rewriting is an old and powerful idea: find a subterm matching the left side of a rule, replace it with the right side, repeat.1 In a compiler, the rules are often familiar algebra or machine facts:

x * 1       -> x
x + 0       -> x
(x * y) / z -> x * (y / z)
x * 2       -> x << 1

The arrow is operational. It says where the optimizer moves next.

That operational arrow is useful because it makes progress concrete. But it is also a commitment. If there are several possible rewrites, the optimizer must pick one. If the rewrite system is not confluent, different choices can land in different normal forms. If some rewrites temporarily increase cost, a local profitability check can reject the only path to a better final expression.

Traditional compilers manage this with pass ordering, fixed points, peephole passes, canonical forms, and a great deal of engineering taste. That work is real. It is also fragile. A new optimization can help one benchmark and block another optimization somewhere else.

Equality saturation changes the arrow back into an equality.

Instead of replacing:

old -> new

it records:

old == new

The old expression remains available. The new expression becomes available. The next rewrite can match either one.

Only at the end does an extraction procedure choose the cheapest expression according to a cost model.

The Data Structure That Holds the Maybe

The production version of this idea uses e-graphs.

An e-graph stores equivalence classes of expressions. If a is equivalent to b, then f(a) must be equivalent to f(b). That closure property is called congruence. Nelson and Oppen’s congruence-closure work is one of the classic roots of the data structure lineage.2

Willsey, Nandi, Wang, Flatt, Tatlock, and Panchekha describe an e-graph as a compact representation of a congruence relation over many expressions.3 The compactness matters because the explicit set of equivalent programs can grow explosively. E-graphs share substructure and merge equivalence classes rather than storing every expression as a separate tree.

Equality saturation uses that representation like this:

  1. Insert the original program.
  2. Repeatedly apply rewrite rules, adding equivalent expressions to the e-graph.
  3. Stop when saturated, timed out, or budgeted out.
  4. Extract the lowest-cost represented program.

Tate, Stepp, Tatlock, and Lerner’s equality-saturation paper framed this as a new optimizer architecture: analyses add equality information to a shared intermediate representation, and a later heuristic picks the final program.4 The key shift is not a clever peephole rule. It is the separation of two jobs that destructive rewriting entangles:

discover equivalences
choose a representative

That separation is why equality saturation feels so different from ordinary rewrite passes. It turns optimization into search without constant regret.

A Tiny Saturation Bench

The lab below is deliberately small.

It is not a production e-graph. It explicitly enumerates a bounded set of expressions so the idea is visible in the browser. A real system like egg uses e-classes, e-nodes, union-find, hashconsing, rebuilding, and e-class analyses to do this compactly and efficiently.3

Still, the tiny version is enough to see the phase-ordering problem.

The Phase-ordering trap scenario starts from:

(a * 2) / 2

The greedy optimizer applies only rewrites that immediately reduce the local cost. It takes the strength-reduction rule and stops at:

(a << 1) / 2

The saturation search keeps that expression, but it also keeps the original shape. That lets it find:

(a * 2) / 2
-> a * (2 / 2)
-> a * 1
-> a

A bounded equality-saturation explorer. The production version stores this space compactly as an e-graph.

Start with Phase-ordering trap.

The greedy result is not wrong. It applied a valid rule. It even lowered the cost immediately. The problem is that local improvement was not the same thing as global extraction.

Now switch to Common-factor cleanup.

The greedy optimizer and saturation search both find:

x * 2 + x * 3
-> x * (2 + 3)
-> x * 5

This is important. Equality saturation is not a claim that greedy rewriting is always bad. Greedy rewriting is often excellent. The claim is narrower: when rewrite order matters, committing early is a source of missed opportunities.

Where the Toy Lab Cheats

The lab cheats in three ways.

First, it stores expressions explicitly. An e-graph stores equivalence classes and shared e-nodes. This is why it can represent many expressions without materializing every tree.

Second, it has a tiny rewrite set. Real optimizers may have hundreds of rules, some purely syntactic and some conditional on analysis facts. The egg paper’s e-class analysis mechanism is important because many optimizations need facts like constant values, free variables, shapes, units, or numerical intervals, not just tree patterns.3

Third, it uses a toy cost model. Production extraction is where engineering judgment re-enters. The cheapest expression depends on the target: latency, instruction selection, vectorization, numerical accuracy, code size, hardware ports, allocation, readability, or some Pareto frontier among them.

Equality saturation does not remove cost modeling.

It gives the cost model more choices.

The Search Is Made of Theorems

There are two ways to view a rewrite rule:

as a command:  replace this with that
as a theorem:  this equals that

The command view is fast and decisive. It is also path-dependent.

The theorem view is slower and more memory-hungry. But it lets independent facts compose. A strength-reduction rule, a division reassociation rule, a constant folder, and an identity rule can all add their little pieces of truth without having to know which pass should run first.

That is the taste of equality saturation. It is a compiler architecture that tries to make local facts commute.

The slogan I find useful is:

Do not ask a rewrite to be profitable.
Ask it to be true.

Profitability belongs at extraction time.

The Pattern Beyond Compilers

This idea shows up wherever we are tempted to optimize by taking irreversible local steps.

In numerical programming, equivalent real expressions can have very different floating-point error. Herbie-style tools use rewrite search to find more accurate forms, and later work has connected that ecosystem to e-graph infrastructure.5

In deep-learning compilers, graph optimizers face algebraic identities, layout choices, fusion choices, and hardware cost models. In CAD and hardware synthesis, the same high-level object may have many equivalent constructions. The common shape is:

many equivalent representations
expensive local commitments
domain-specific cost function

An e-graph is a way to hold the ambiguity long enough to make a better choice.

That is why the tiny (a * 2) / 2 example is not trivial. It is the smallest version of a serious design principle:

separate discovery from choice

Destructive optimization mixes them together.

Equality saturation pulls them apart.

Source Notes

  1. Nachum Dershowitz and Jean-Pierre Jouannaud, “Rewrite Systems,” in Handbook of Theoretical Computer Science, Volume B, 1990. A freely available draft is hosted by Tel Aviv University: Rewrite Systems. ↩

  2. Greg Nelson and Derek C. Oppen, “Fast Decision Procedures Based on Congruence Closure”, Journal of the ACM, 1980. ↩

  3. Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha, “egg: Fast and Extensible Equality Saturation”, POPL 2021. ↩ ↩2 ↩3

  4. Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner, “Equality Saturation: A New Approach to Optimization”, Logical Methods in Computer Science, 2011; earlier version POPL 2009. ↩

  5. Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock, “Automatically Improving Accuracy for Floating Point Expressions”, PLDI 2015. For a practical bridge between Herbie and equality infrastructure, see Flatt and Zhang, “egglog In Practice: Automatically Improving Floating-point Error”. ↩