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.
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.
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.
Really nice explanation and visuals!
There is one part I want to quibble with:
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*0andx*0, and later learn that they’re equal (both zero), you wouldn’t want to infer that2andxare equal.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.
Didn’t you hear? A fix was released—all men are socrates now.