Help debugging seemingly-erroneous backwards rewrites

[silversquirl]

The following rewrites for a pure language are able to optimize expressions such as (let a 0 (let b a b)) to 0. However, they are also able to optimize the same expression to a, which is obviously invalid as a is unbound in that context.

rw!("let-distrib"; "(let ?v ?x (let ?u ?y ?body))" => "(let ?u (let ?v ?x ?y) (let ?v ?x ?body))"),
rw!("let-delete"; "(let ?v ?x ?a)" => "?a" if is_not_equal_atom(var("?v"), var("?a"))),
rw!("let-cancel"; "(let ?v ?x ?v)" => "?x"),

I find explanation provided for this proof somewhat confusing, as it doesn't show how the let-distrib equivalence is found.

(let a 0 (let b a b))
(let a (Rewrite<= let-delete (let b a 0)) (let b a b))
(Rewrite<= let-distrib (let b a (let a 0 b)))
(let b a (Rewrite=> let-delete b))
(Rewrite=> let-cancel a)

Asking it to narrow in on the specific issue point (the proof that (let a (let b a 0) (let b a b)) is equivalent to (let b a (let a 0 b))) doesn't help at all:

(let a (let b a 0) (let b a b))
(Rewrite<= let-distrib (let b a (let a 0 b)))

Is there any way to have it show more information on these backwards rewrites so I can figure out how it's finding the equivalences?

(Full code example, for reference)

[mwillsey]

pinging @oflatt, the resident proofs wizard 🧙

[oflatt]

Hi @silversquirl, great to see people using this feature for debugging.

The second proof you show is as specific as it gets: it's exactly one rewrite application.
Looking at your rule, the substitution is ?v = b, ?x = a, ?u = a, ?y = 0, body = b.
Substituting on the right-hand side of the rule, you get your result: (let a (let b a 0) (let b a b)).

Did that help? "Backwards" rewrites are just like forwards rewrites, but the right-hand side of the rule application is the previous term.
Maybe in future egg versions we should optionally display the substitution

[silversquirl]

I was under the impression that in order to apply a rewrite in reverse, egg first had to create an equivalence between them separately?
ie. a rule (+ ?a 0) => ?a allows rewriting (+ x 0) into x but not vice versa, unless there is an instance of (+ x 0) somewhere else in the graph (which would then create an equivalence between (+ x 0) and x meaning egg can apply that equivalence elsewhere)

I think I've managed to build a slightly better understanding of what's going on using explain_existance, but I'm still not sure how to restrict my rules sufficiently to stop it from propagating things further up the tree. Perhaps with the help of some analysis to get free vars? I'm not exactly sure how that'd work though.

The other idea I've had is to change my IR to make it unordered and mostly flat, and then build a dependency graph after the fact to create an ordering for codegen. Would be interested to hear thoughts from people more knowledgeable than me :)

[oflatt]

The rule isn't actually being applied in "reverse". Egg is applying it forwards, but we happen to present it in reverse when you get the actual explanation.

It sounds like you are on the right track with understanding why your bug is happening. We actually have a similar test in the egg test suite which has an analysis tracking free variables:
https://github.com/egraphs-good/egg/blob/main/tests/lambda.rs