1. 35
cole-k.com
1.

1. 2

Really nice explanation and visuals!

There is one part I want to quibble with:

Suppose we’ve discovered that `(a*2)/2` is equal to `(a<<1)/2` and want to add it.

But wait! Once we know that they’re in the same e-class, we can now reason about their arguments being equal.

I think this is getting the right answer for the wrong reason. In this case we do know that `(a*2)` == `(a<<1)`, but that’s because a rewrite rule told us directly. You want to tell the egraph `(a*2)` == `(a<<1)` and let it derive `(a*2)/2` == `(a<<1)/2`, not the other way around. Once you know the arguments are equal, then you know the parent expressions are equal.

For example, if you start with two unrelated expressions `2*0` and `x*0`, and later learn that they’re equal (both zero), you wouldn’t want to infer that `2` and `x` are equal.

1. 2

Ah that’s a good point. I wanted to introduce how equality can propagate throughout the e-graph in that section but I didn’t want to yet discuss applying rewrites directly.

I’m not sure whether I should drop the more compact e-graph where `(a*2) == (a<<1)`… some prior readers were confused by this translation (perhaps now because of what you’re saying) and we get to it in the next section anyway.

Edit: Thanks. Fixed in an update to the post.

2. 1

For example, if you start with two unrelated expressions `2*0` and `x*0`, and later learn that they’re equal (both zero), you wouldn’t want to infer that `2` and `x` are equal.

Didn’t you hear? A fix was released—all men are socrates now.