Building a state-of-the-art program optimizer, synthesizer, or verifier is still a gargantuan task for even programming language (PL) experts. Much of this challenge stems from the fact that term rewriting, a ubiquitous approach to manipulating programs, only works with one version of a program at a time. As a result, the system builder must carefully consider every program manipulation, lest they accidentally “take a wrong turn” and miss out on optimization opportunities. For non-PL-experts, these difficulties prevent application of PL techniques to domains that might otherwise greatly benefit from them.

This talk will describe a data structure called the e-graph and a technique called equality saturation that together allow one to store and manipulate many equivalent versions of a program simultaneously. Recent advances like delayed congruence closure and lattice-based “e-class analyses”, both embodied in the egg e-graph toolkit, have made this approach fast and flexible enough for academic and industrial use in areas including deep learning, carpentry, 3D design, and floating point arithmetic. This talk will also present recent discoveries that connect equality saturation to relational databases. The result is faster, simpler, and theoretically optimal implementations of equality saturation.