[−][src]Module egg::tutorials::_01_background
Concepts: egraphs and equality saturation
An egraph is a data structure that powers the equality saturation optimization technique.
Both egraphs
(Gregory Nelson's PhD Thesis, 1980)
and equality saturation
(Tate et. al., 2009)
were invented before.
egg
aims to make them easy, extensible, and efficient.
This tutorial will approach these concepts at a high level. More detail can be found in our paper.
Why any of this?
When building pretty much any tool relating to programming languages, you'll typically be working with terms from your language (we will use the words term, expression, and program interchangeably). You may be trying to:
 Convert a term to a "better", equivalent term (optimization);
 Build a term from scratch according to a specification (synthesis);
 Or show that two terms are equivalent (verification).
Term rewriting is common technique for working with terms toward any of these goals. You start with a term t and a set of rewrites, each of which take the form l → r. For each rewrite, you try to match the pattern l against the term t, generating a substitution σ at some subterm, and then you apply that substitution to the righthand pattern r and replace the matching subterm.
For example, consider the term 42 × (7 + 7) and the rewrite x + x → 2 × x:
 The lefthand side would match at the subterm 7 + 7, generating the substitution σ = {x: 7}.
 Applying the substitution gives r[σ] = 2 × 7. (r[σ] means apply the substitution σ to r)
 Replacing the matched subterm 7 + 7 with r[σ] = 2 × 7 gives the result: 42 × (2 × 7).
One issue with term rewriting (and other programming language techniques that involve manipulating terms) is the matter of choice. Rewriting is destructive, meaning that once you do a rewrite, the initial term is gone. If you have many rewrites to choose from, picking one is like choosing a fork in the road: going back and choosing another way is expensive or impossible, so you're committed to the path you've chosen. Furthermore, picking the right rewrite at the right time is very difficult in general; sometimes, a choice that seems good locally may be wrong globally.
As an example, a C optimizer would like to rewrite a * 2
to the cheaper a << 1
.
But what about (a * 2) / 2
?
A greedy, local approach will take a "wrong turn" resulting in (a << 1) / 2
,
which is better than the input expression
but hides the fact that we could have canceled the multiplication and division.
There are some techniques to mitigate this (backtracking and valuenumbering), but fundamentally, the only way around it is to take all choices at the same time. But rewriting is destructive, so applying n rewrites to a term results in n terms, and then applying n rewrites to each of those n terms yields n^{2} more terms, and so on. If you want to explore m "layers" deep in this tree, you'll have to store n^{m} terms, which is prohibitively expensive.
Egraphs can solve this representation problem. When rewriting a bunch of terms, the results are often structurally similar. Egraphs can store large sets of similar expressions very compactly. Using egraphs, you can apply many rewrites simultaneously without a multiplicative growth in space. Equality saturation is a technique to do this kind of rewriting for program optimization.
What's an egraph?
An egraph (/'igraf/) is a data structure to maintain
an equivalence relation
(really a congruence relation, see the next section)
over expressions.
An egraph is a set of equivalence classes (eclasses),
each of which contains equivalent enodes.
An enode is an operator with children, but instead of
children being other operators or values, the children are eclasses.
In egg
, these are represented by the EGraph
, EClass
, and
Language
(enodes) types.
Even small egraphs can represent a large number of expressions, exponential in the number of enodes. This compactness is what makes egraphs a compelling data structure. We can define what it means for represent (or contain) a term as follows:
 An egraph represents a term if any of its eclasses do.
 An eclass represents a term if any of its enodes do.
 An enode
f(n1, n2, ...)
represents a termf(t1, t2, ...)
if enodeni
represents termti
.
Here are some egraphs. We picture eclasses as dotted boxes surrounding the equivalent enodes. Note that edges go from enodes to eclasses (not to other enodes), since enodes have eclasses as children. Don't worry about how they are made just yet, we'll get to rewriting soon.
An egraph can be queried for patterns through a procedure called ematching
(matching up to equivalence),
which searches the egraph for eclasses that represent terms that match a given pattern.
egg
's ematching
(inspired by
De Moura and Bjørner)
is done by the Searcher
and Pattern
APIs.
There are two core operations that modify the egraph:
add
which adds enodes to the egraph, and
union
which merges two eclasses.
These operations can be combined to do rewriting over the egraph.
Critically, this rewriting process is only additive,
meaning that the egraph never forgets old versions of terms.
Additionally, rewrites add entire classes of terms at a time.
To perform a rewrite l → r over an egraph,
you first search l in the egraph, yielding pairs of (c, σ),
where c is the matching eclass and σ is the substitution.
Then, you add
the term r[σ] to the egraph
and union
it with the matching eclass c.
Let's put it all together with an example referring to the four egraphs in the image above.
 The initial egraph represents the term (a × 2) / 2. Since each eclass only has one enode, the egraph is basically an abstract syntax tree with sharing (the 2 is not duplicated).
 Applying the rewrite x × 2 → x << 1 has recorded the fact that a × 2 = a << 1 without forgetting about a × 2. Note how the newly added a << 1 refers to the existing "a" enode, and the "<<" enode has been unioned into the same eclass as the equivalent "×" enode where the pattern x × 2 matched.
 Applying rewrite (x × y) / z → x × (y / z) realizes that division associates with multiplication. This rewrite is critical to discovering the cancellation of 2s that we are looking for, and it still works despite the fact that we applied the "wrong" rewrite previously.
 Applying rewrites x / x → 1 and 1 × x → x doesn't add any new enodes, since all the enodes were already present in the egraph. The result only unions eclasses, meaning that egraph actually got smaller from applying these rewrites, even though it now represents more terms. In fact, observe that that the topright "×" enode's left child is itself; this cycle means the eclass represents the infinite (!) set of terms a, a × 1, a × 1 × 1, and so on.
Invariants and Rebuilding
An egraph has two core operations that modify the egraph:
add
which adds enodes to the egraph, and
union
which merges two eclasses.
These operations maintains two key (related) invariants:

Congruence
An egraph maintains not just an equivalence relation over expressions, but a congruence relation. Congruence basically states that if x is equivalent to y, f(x) must be equivalent to f(y). So as the user calls
union
, many eclasses other than the given two may need to merge to maintain congruence.For example, suppose terms a + x and a + y are represented in eclasses 1 and 2, respectively. At some later point, x and y become equivalent (perhaps the user called
union
on their containing eclasses). Eclasses 1 and 2 must merge, because now the two "+" operators have equivalent arguments, making them equivalent. 
Uniqueness of enodes
There do not exist two distinct enodes with the same operators and equivalent children in the eclass, either in the same eclass or different eclasses. This is maintained in part by the hashconsing performed by
add
, and by deduplication performed byunion
andrebuild
.
egg
takes a delayed approach to maintaining these invariants.
Specifically, the effects of calling union
(or applying a rewrite,
which calls union
) may not be reflected immediately.
To restore the egraph invariants and make these effects visible, the
user must call the rebuild
method.
egg
's choice here allows for a higher performance implementation
Maintaining the congruence relation complicates the core egraph data
structure and requires an expensive traversal through the egraph on
every union
.
egg
chooses to relax these invariants for better performance, only
restoring the invariants on a call to rebuild
.
The paper on egg
goes into greater detail on why this design choice makes
things faster.
See the rebuild
documentation for more information on
what it does and when you have to call it.
Note also that Runner
s take care of this for you, calling
rebuild
between rewrite iterations.
Equality Saturation
Equality saturation
(Tate et. al., 2009)
is a technique for program optimization.
egg
implements a variant of equality saturation in the Runner
API that
looks like the following pseudocode:
fn equality_saturation(expr: Expression, rewrites: Vec<Rewrite>) > Expression { let mut egraph = make_initial_egraph(expr); while !egraph.is_saturated_or_timeout() { let mut matches = vec![]; // readonly phase, invariants are preserved for rw in rewrites { for (subst, eclass) in egraph.search(rw.lhs) { matches.push((rw, subst, eclass)); } } // writeonly phase, temporarily break invariants for (rw, subst, eclass) in matches { eclass2 = egraph.add(rw.rhs.subst(subst)); egraph.union(eclass, eclass2); } // restore the invariants once per iteration egraph.rebuild(); } return egraph.extract_best(); }
Most of this was covered above, but we need to define two new terms:
 Saturation occurs when an egraph detects that rewrites no longer add new information. Consider the commutative rewrite x + y → y + x. After applying it once, the second time adds no new information since the egraph didn't forget about the initial x + y terms. If all the rewrites are in this state, we say the egraph is saturated, meaning that the egraph encodes all possible equivalences derivable from the given rewrites.
 Extraction is a procedure for picking a single represented from an eclass
that is optimal according to some cost function.
egg
'sExtractor
s provide this functionality.
Put together, equality saturation explores all possible variants of a program that can be derived from a set of rewrites, and then it extracts the best one. This solves the problem of choice describes above, as equality saturation essentially applies every rewrite every iteration, using the egraph to avoid exponential explosion.
It sounds a little too good to be true,
and while it definitely has its caveats,
egg
addresses many of the shortcomings from this approach,
making it feasible to apply on realworld problems.
We've already discussed how rebuilding makes egg
's egraphs fast,
and later tutorials will discuss how Analysis
makes this approach flexible
and able to handle more than just syntactic rewriting.