Now it’s time to lift up the curtain a bit more, and consider what happens when we equate x-x = Zero.1
This equation has an interesting property, the left-hand-side refers to a variable x, which does not occur in the right-hand side.
Recall that in any equation, we are always free to bijectively rename all variables using the “renaming rule”:
Thus from x-x = Zero we can directly infer y-y = Zero.
And thus it follows x-x = y-y.2
If we were to express this situation in a “Chapter I” slotted e-graph, we might attempt this:
c0(x) := x
c1(x) := Zero | c0(x) - c0(x)
But if we recall the “semantics” c1(x) = {Zero} ∪ { a - b | a ∈ c0(x), b ∈ c0(x) }, we notice a problem.
The e-classes c1(x) and c1(y) overlap in Zero, but are not the same.
For example c1(x) contains x-x, but c1(y) does not.
This is not how equivalence classes work! If they overlap, they have to be the same!
This effectively means that the slotted e-graph did not internalize the fact x-x = y-y (or c1(x) = c1(y)), that we had just proven before.
The property c1(x) = c1(y) has a useful characterization, it describes exactly constant functions.
We can interpret this as a hint that the parameter x of c1(x) should probably go away.
In order to get rid of the parameter x, while still being able to express x-x, y-y, …, we require redundant variables:
c0(x) := x
c1 := Zero | c0(_x_) - c0(_x_)
Now, the parameterized e-class c1 stopped being parameterized3, however it now contains a redundant variable _x_.
The semantics of this is c1 = {Zero} ∪ { a - b | a ∈ c0(x), b ∈ c0(x), x variable }, and thus we effectively express c1 = {Zero, x-x, y-y, ...} as desired!
Notice that this semantics is exactly the union of all these e-classes c1(x), c1(y), … that were overlapping but not equivalent in the previously attempted semantics.
Thus, in typical e-graph fashion, we merged a couple of overlapping e-classes into one.
And that’s about it. Redundant variables are an extension that allow you to handle equations,
where the left, and the right-hand-side disagree on the set of variables. Whenever x comes up on one side, but not the other, it will become a redundant variable.
Finally, one thing to keep in mind is that the shape computation does not distinguish between redundant variables and normal variables.
Both kinds of variables will just be renamed to 0, 1, ... as explained prior.
When seeing the equation x-x = y-y, someone might have already figured out how this could relate to binders.
Binders have a property called alpha-equivalence; for example λx. x = λy. y is a consequence of alpha-equivalence.
It basically states that you are free to rename any bound variables in a term, and you will obtain an equivalent term.
So, the trick to encode binders in slotted e-graphs is to just have a normal λx. _ e-node type.4
And whenever some e-class c(x, y, z) contains an e-node λx. _,
you derive c(x, y, z) = c(x', y, z) and let the redundancy system take it from there.
This way, the slotted e-graphs will mark x (and x') as redundant, and thus we’re allowed to freely “alpha-rename” them from then on.
Recall from the “Theory” section from chapter one, that we only allow “bijective” renaming of variables. Among other things, this was supposed to prevent naming collisions when expressing binders.
In this section, we will see now that our semantics of redundant variables will need a final tweak to fully respect this.
For that, let’s consider the example λx. λy. x+y:
c0(x) := x
c1(x,y) := c0(x) + c0(y)
c2(x) := λ_y_. c1(x, _y_)
c3 := λ_x_. c2(_x_)
When we look at the semantics of c2(x), we obtain
c2(x) = { λy. a | a ∈ c1(x, y), y variable }But there’s an issue: The semantics of c2(x) also includes λx. x+x, which is not alpha-equivalent to λy. x+y!
This is, as in the semantics of redundant variables, we had forgotten that we’re only allowed to do “bijective” renamings.
In particular, there is now a looming variable collision between x and y.
To address this, we simply need to tweak the semantics of redundant variables, so that the redundant variable will be chosen to not collide with any other variables from the equation:
c2(x) = { λy. a | a ∈ c1(x, y), y variable, y ≠ x }This “y ≠ x” constraint prevents c2(x) from containing λx. x+x, resolving the naming collision.
As noted in “Chapter I”, learning new equations and simplifying accordingly can sometimes (by congruence) yield new equations.
A similar thing happens with redundant variables.
If you know that c1(x) = x-x gets simplified to c1 without a parameter,
then all “parent” e-classes (like c4(x, y, z) = c1(x) + c2(y, z)) may lose the dependency on this parameter aswell (like c4(y, z) = c1 + c2(y, z)).
In an extreme case, when equating x=y, then the unique variable e-class c0(x) := x gets a redundant variable c0 := _x_,
and all other e-classes lose all their variables as a consequence of this. Then the slotted e-graph degenerates to a conventional e-graph.
I write “Zero” to prevent being ambiguous with the numeric variables 0, 1, 2 that we use in shapes. ↩
This works generally. If you have an equation t1 = t2, where x comes up in t1, but not in t2, you can always derive t1[x := y] = t2 and thus t1 = t1[x := y] (assuming y fresh). ↩
If you don’t like changing the arity of symbols from c1(x) to just c1: In the implementation we instead declare a new e-class c2, and add the unionfind equation c1(x) := c2, replacing each occurrence of c1(x) with c2. ↩
One thing that is a bit special about the λ-node is that, next to the “variable” e-node, it’s a node that takes not only subterms, but also a variable (the bound one) directly. If you don’t do this, you get weird terms like λ(x+0). _ when x = x+0 (but there’s also other ways to fix that). ↩