by Max Willsey on Oct 1, 2026
Equality saturation is a program optimization technique built around storing and rewriting large equivalence classes of programs in a data structure called an e-graph. It was invented by Tate et al. in POPL 2009. Our paper at POPL 2021, “egg: Fast and Extensible Equality Saturation”, generated a lot of interest in the technique and its applications. That same year, I wrote a post on this topic for this very blog!
Since then, a lot has happened! egg itself has been used directly in a variety of industrial and academic applications. More importantly, it has been superseded by other works that have developed more useful or efficient approaches to equality saturation, some of which I will highlight in this post. At venues like PLDI, POPL, and OOPSLA we have seen a growing number of works either working on or using equality saturation in some form.
This year was a particularly big year!
- The
eggpaper was selected as a CACM Research Highlight (accompanied by a great technical perspective from Nadia Polikarpova, thanks Nadia!). - A Dagstuhl seminar on equality saturation brought together researchers from around the world to discuss progress and challenges in this area.
- The EGRAPHS Workshop held its fifth iteration at PLDI 2026, with a great program and participation, making it again one of the largest workshops at PLDI. In addition to the workshop, there was a whole “Equality Saturation” session at the conference!
With all of those developments, it’s time for another blog post! Here I’ll try to highlight some key developments and challenges in equality saturation. I also want to use the benefit of hindsight to offer my perspective on why this line of work has found success, and how it might continue to evolve.
The theme here (and the cheekiness in the title) is “incompleteness”, in two ways. The first is technical: a thread running through many parts of this work is that we are repurposing techniques from automated theorem proving to the setting of program optimization. This means taking decision procedures (which are sound and complete) and often giving up on completeness to gain flexibility. Program “optimization” is somewhat of a misnomer anyway: unlike optimization in other mathematical contexts where the optimal is the only correct answer, here we often accept a better program as long as it’s equivalent to the original. The second sense is the colloquial one: the work here is not finished. I will try to highlight how works in the community are either addressing or simply dealing with the current weaknesses of equality saturation to apply it to program optimization in various ways.
E-Graphs and Equality Saturation, briefly
This post won’t offer a full background of equality saturation. For that, consider the recent CACM version of the egg paper, or one of the many blog posts that Philip Zucker has collected on his Awesome E-graphs page. But here I’ll give a very brief overview.
An e-graph is a data structure that represents an equivalence relation over terms. The picture below shows four e-graphs, each one representing a larger equivalence relation than the previous. E-graphs have been used in automated reasoning since the 70s for solving congruence closure. In 2009, Ross Tate and co-authors proposed equality saturation, a technique for doing program optimization via non-destructive rewriting in an e-graph. Briefly, the technique works as follows:
- Start with an e-graph representing the initial program. (See the left-side e-graph below representing the term
(a * 2) / 2.) - Apply rewrites non-destructively: for every match of a rule’s left-hand side, add the right-hand side to the e-graph and union the two e-classes. Nothing is ever lost, so the process is less sensitive to the order in which the rules are applied. The left-most two e-graphs in the picture below illustrate the application of the rewrite:
a * 2 -> a << 1. - Repeat until the e-graph saturates, meaning no rule can add anything new, or until a resource limit is reached. Saturation will not always be possible.
- Extract the best term from the resulting e-graph according to some cost function.
[Figure: Four e-graphs, each one representing a larger equivalence relation than the previous. Gray indicates what didn’t change from the previous image.]
Incomplete Algorithms
While equality saturation is built on e-graphs and congruence closure (which is complete, i.e. it’s a decision procedure), equality saturation itself is incomplete. Often saturation is not possible or practical, which is an obvious source of incompleteness since there are missing equivalences that the algorithm didn’t discover. Even in cases where equality saturation does saturate, that doesn’t mean it will prove a certain equality derivable by the rules (Zhang et al.’s Semantic Foundations of Equality Saturation digs into this). When used for program optimization, this means that you will get a program that is equivalent to the input, but you will not get a program that is guaranteed to be optimal. In practice, this means that equality saturation (like many other approaches in program optimization) amounts to a best-effort technique.
Trading off completeness comes with two upsides. First, there are fewer limitations on how a client can “bolt on” or combine reasoning with an equality saturation engine. Recent works like Sofia Brookie’s Masters thesis, Kong et al. at PLDI this year, and others explore this notion of “e-graphs modulo theories”. These build on a rich history of works for automated reasoning that (very sensibly) have the burden of maintaining completeness. But in our setting of equality saturation, something is better than nothing: you’d rather have support for some level of theory reasoning, even if incomplete, since often it only takes a little bit of extra juice to unlock other optimizations. This line of work is early, and it remains to be seen how useful these incomplete theories are in many domains.
The second upside is a bit more nuanced, but something I’ve observed in many projects that use equality saturation. It relates to performance and control. Many equality saturation projects are more involved than a simple plug-and-play approach, of putting in rewrite rules, pressing go, and getting out a term. That kind of workflow is certainly something to aspire to, and is more akin to what you might do with a decision procedure. Instead, many equality saturation projects use egg or whatever other toolchain in a “white-box” way, exerting some level of control over the equality saturation process.
Early egg projects like Szalinski, a 3D CAD decompiler did this in an ad-hoc way, using Rust code to insert certain “potentially profitable” equations into the e-graph but not others. Modern equality saturation tooling like egglog has a scheduling feature that allows programmatic control over rule application. Kœhler et al.’s Guided Equality Saturation operates at an even higher level, letting the user sketch intermediate steps when the search space is too big to cross in a single hop.
Approaches like these are allowed because equality saturation maintains soundness but gives up on completeness. That is a low bar! But it’s a useful one, since it means the pieces can be swapped, tuned, scheduled, and interrupted by people who are not interested in proving anything about the whole.
An Incomplete Mission
The second sense of “incomplete” is the plain one: the work isn’t finished.
egg shipped with a relatively small surface: an e-graph, e-matching, rebuilding, e-class analyses, and a hook for extraction. It had no support for binders, no support for associative/commutative operators, no proof production, no support for contextual equality, and a rule scheduler that was little more than a heuristic. At the time those all felt like things we simply hadn’t gotten to yet. With hindsight I think the holes were the most useful part of the design, because each one turned out to be a place where somebody else did better work than we would have. It also cemented the fact that egg is certainly not the only or best way to do equality saturation.
The clearest case is that people rebuilt the engine itself. egglog replaced egg‘s rewrite-rule API with a Datalog-style query language, unifying equality saturation with Datalog; it is the tool I would point most new users toward today. Metatheory.jl brought e-graphs to Julia, egglog-python brought them to Python, and there are bindings, ports, and reimplementations in several other languages besides. Two different recent works (eqsat dialect and DialEgg) embed equality saturation into MLIR.
Other new works offer extensions to the e-graph giving it new capabilities. Slotted E-Graphs at PLDI 2025 makes bound variables a first-class part of the data structure. Colored E-Graphs and Versioned E-Graphs add the ability to work with different, overlapping equivalence relations instead of just one.
Another example is the Cranelift compiler’s mid-end, which Chris Fallin rearchitected around e-graphs in 2022. Chris built a prototype using egg, but it did not meet the performance requirements of a production WASM compiler like Cranelift. Chris started innovating, throwing out many features that at the time I would have considered essential to equality saturation, like congruence closure. The result was ægraphs, or “acyclic e-graphs”, which trade off many features of egg-style e-graphs (including the cycles that can form to represent infinite families of terms) for a much more performant implementation that strictly manages its growth and memory consumption.
There are still many problems to solve and applications to build! One of the strengths of equality saturation is the ability to defer a difficult decision until extraction time. In settings like partial evaluation or inlining, it can be very difficult to tell where doing a particular transformation is worth it, since the benefit might only be apparent much later. These transformations are the workhorses of compilers, and it seems like equality saturation could be a natural fit! However, while the recent Slotted E-graphs work yields some progress towards representing binding structures in an e-graph, efficiently handling substitution and beta-reduction is an open problem.
Looking Forward
Equality saturation is fundamentally incomplete, and that has turned into a strength rather than a weakness. On the technical side, many works have embraced the incompleteness inherent in program “optimization” to offer more flexibility, performance, or interactivity than a complete solution could have. On the project side, the fact that equality saturation has many directions for extension and improvement has led to a lot of great research from a growing community, and I’m excited to see what happens next.
If any of that sounds fun, please come join us. The EGRAPHS workshop happens every year at PLDI, there are monthly community meetings on Zoom, and egraphs.org has links to the Zulip where most of the day-to-day conversation happens. Philip Zucker’s Awesome E-graphs is another great resource for learning about this area.
Bio: Max Willsey is an Assistant Professor in EECS at UC Berkeley. His research aims to make program optimization more robust, powerful, and accessible.