In this blog post I attempt to give a simple and concise explanation of slotted e-graphs.
For that we’ll start in Chapter I with a basic version,
and in Chapter II we will see what happens if you dare to equate x-x = 0;
and finally in Chapter III we will see what happens if you dare to equate x+y = y+x.
Interestingly, binders just “fall out for free” in Chapter II as a consequence of redundancies, so they do not come up in Chapter I.
I intend to ignore e-matching and proof production, as they aren’t really remarkable for slotted e-graphs – but tedious.
First, what is an e-graph?
An e-graph stores a bunch of terms and equations among them, by grouping equivalent terms into equivalence classes (“e-classes”).
For example, we might represent the equal terms -(x-y) = (y-x) as follows:
c0 := x
c1 := y
c2 := c0 - c1
c3 := - c2 | c1 - c0
Every c0, ..., c3 corresponds to an “e-class”, whereas the terms on the right (eg. c0 - c1) correspond to “e-nodes”. 1
A slotted e-graph is extending e-graphs by a notion of built-in variables (and binders).
If we convert this conventional e-graph to a slotted e-graph, every e-class will be parameterized by the variables (aka slots) that it contains:
c0(x) := x
c1(y) := y
c2(x, y) := c0(x) - c1(y)
c3(x, y) := - c2(x, y) | c1(y) - c0(x)
One can visualize a parameterized e-class (eg. c3) as a function, that takes in variable names (x, y) and yields a set of terms:
c3(x, y) = {-a | a ∈ c2(x, y) } ∪ { a - b | a ∈ c1(y), b ∈ c0(x)}These parameterized e-class functions recursively call each other to build up all the terms they represent.2 Thus, after some function inlining we end up with:
c3(x, y) = { -(x - y), y - x }As parameterized e-classes can be seen as functions, the variable names (i.e. function parameters) chosen in every e-class have no particular meaning, and can be renamed at any point.
We could for example re-define c2 equivalently as c2(f, d) := c0(f) - c1(d) if we wanted to.
This is one crucial property of variables: The names you choose do not matter!
As each term should be represented only in a single e-class, e-graphs must detect when different e-classes share a common e-node. In order to achieve this they use the “hashcons”, which is supposed to map each e-node to the unique e-class that contains it.
In Slotted E-Graphs we want a stronger notion of deduplication: If two e-nodes (or terms) are equal up to renaming3 of variables, they should be represented by the same parameterized e-class.
The problem with the hashcons is that two e-nodes that are equal up to renaming can definitely still hash to different values. Think hash("x+y") != hash("a+b"),
so we require a “name-independent representation” of e-nodes (called its shape) that we can use for the hashcons.
To compute the shape of an e-node, we rename all variables to “numeric variables” (0, 1, …) based on the order of their first occurrence.
For example the e-node c3(x, y, z) + c4(w, x) would have the shape c3(0, 1, 2) + c4(3, 0).
In other words, the shape of an e-node is the lexicographically smallest e-node that is equal up to renaming to it. (Assuming the lexicographical ordering 0 < 1 < 2 < ...)
If we now come back to the example from before, and populate the hashcons in the way we have just described,
we will notice that both x and y will result in the shape 0, yielding a “hashcons-collision”.
Our hashcons-invariant forces us to map hashcons[0] to both c0 and c1, which means that we have to merge these e-classes.4
How do we know that these e-classes can be safely merged? Recall that the choice of variable names does not matter,
hence instead of c0(x) = x, we could also have written c0(0) = 0. And similarly we obtain c1(0) = 0;
and from that we can infer c0(0) = c1(0).
So now we can simplify our slotted e-graph, by replacing all occurrences of c1(0) with c0(0), where 0 matches against any variable:
c0(x) := x
c2(x, y) := c0(x) - c0(y)
c3(x, y) := - c2(x, y) | c0(y) - c0(x)
c1(0) := c0(0)
We remember how we eliminated c1 using this final equation c1(0) := c0(0). We will clarify this more in Unionfind.
This simplification enables another one:
The e-classes c2 and c3 now each contain an e-node with shape c0(0) - c0(1), that we will detect when populating the hashcons.
From these e-nodes we infer the equation c2(0,1) = c0(0) - c0(1) = c3(1,0).
This equation is a bit more interesting than the one we had before. We have equated the e-classes c2 and c3, but there’s a literal twist:
The first variable in c2, corresponds to the second variable in c3 and vice versa.
Using this new equation, We can now replace c3(1,0) with c2(0,1), where again 0, 1 can match against any variables:
c0(x) := x
c2(x, y) := - c2(y, x) | c0(x) - c0(y)
c1(0) := c0(0)
c3(0, 1) := c2(1, 0)
Whenever you merge two classes, one will be the “canonical e-class” (in this case c2), and the other e-class (c3) will just point to that canonical e-class.
This “pointer” c3(0, 1) := c2(1, 0) will be stored in a unionfind datastructure, it is expressed as unionfind[c3] = c2(1, 0).5
When applying path compression to the unionfind, one has remember to compose these re-orderings;
just like c2(x, y) := c1(y, x) and c1(x, y) := c0(y, x) implies c2(x, y) = c0(x, y).
Before defining the notion of “redundancies” in Chapter II, I want to lay some more groundwork to formally clarify what we’ve been up to in this chapter.
An e-graph computes the congruence closure for a given set of terms. In other words, it finds all the equations that you can derive from your input equations via transitivity, symmetry, reflexivity and congruence.
A slotted e-graph extends these equational rules by one more variable-specific rule, namely the “renaming rule”:
t1 = t2, then t1[σ] = t2[σ] holds for any bijective renaming σTo make an example, with this rule we can derive that
f(x, y) = g(x) implies f(a, b) = g(a), using the renaming σ(x) = a, σ(y) = b.
However, crucially, with this rule we can not derive that
f(x, y) = g(x) implies f(a, a) = g(a). As you would require the non-bijective renaming σ(x) = a, σ(y) = a for that.
And as we’ll see in Chapter II, this restriction is what allows us to express binders in the first place. Binders have the typical problem of “naming collisions” where two names that originally meant different things are renamed to the same name, creating a collision. However, bijective renamings are literally incapable of producing such naming collisions, and are thus a useful framework to express binders.6
Finally, I want to point out that Chapters II and III are consequences of the general problem definition (congruence closure with the renaming rule) we have sketched here. The slotted e-graph described in this chapter alone is not capable of proving every derivable equation in this logic yet. But luckily, on the way to reach that milestone, binders will fall out as a useful side-product.
If you squint a bit, this looks like a context-free grammar. In general, E-Graphs can be seen as context-free grammars, where non-terminals correspond to e-classes, and production rules correspond to e-nodes. They just have the extra constraint that their non-terminals have no overlap. I’m sure people knew this since the dawn of time, but it’s cool and I never see people use that connection somehow. ↩
Technically, for recursive e-classes these functions would not terminate, but I hope it’s clear what I mean. Think of these sets as the smallest fixed-points under these equations. ↩
Technically, it would be “equal up to a bijective(!) renaming”. As x-y and x-x should not be considered “equal up to renaming”. ↩
In general, you just have one variable e-class in a slotted e-graph. After all, all variables are equal up to renaming. ↩
In the current implementation, we actually store unionfind[c3] = (c2, [x := y, y := x]), as it uses canonical names (x, y) instead of canonical positions (0, 1). But that’s a matter of taste. ↩
If I understood it correctly, the people doing nominal rewriting also came to this conclusion. ↩