problems with unsimplified pattern searchers

[nlewycky]

The setup is that I have a destructive rewrite rule like rewrite!("mul-0"; "(* 0 ?a)" => "0") which as I understand it never runs backwards to turn 0 into (* uninstantiated-var 0). I also have rewrite rules which are derived from user input, and in one case I introduced a rule like (+ (+ (* 0 (* x x)) (* 7 x)) 1) as a search pattern. This never matched anything, because of the multiply by zero on the (* x x) term.

I've thought about a preprocess to remove (* 0 x) myself, which I could do for "mul-0", however those new rewrite rules derived from user input can also be destructive (having an uninstantiated variable on the left but not the right). One thing I tried was adding the search side of the rule as an expr to the graph in the hopes that the graph would simplify it and the searcher could follow the new expression, but it does not work that way. Making a variant on pattern searcher which does work that would seems like it would be difficult and require explanations enabled to track where the pattern variable went.

Any ideas on how to handle this?

[mwillsey]

I'm not exactly sure what you mean by destructive in this context; rewrite!s are not "destructive" as far as I understand the term.

Perhaps you could try "optimizing" the patterns? For example, insert a term that looks like (+ (+ (* 0 (* x x)) (* 7 x)) 1) (ensuring that you use a fresh x), optimize and extract, and then convert the result back into a pattern. Could that work for you?

[nlewycky]

"Destructive" meaning that the rewrite "destroys information" because the substitution variable on the left isn't present on the right. "(* ?x 0)" to "0" has this property as does "(exp ?x 0)" to "1", but "(+ ?x 0)" to "?x" does not because it's possible to undo the rewrite given the right-hand-side and knowing which rewrite was applied.

It makes sense that egg doesn't turn every "0" into "(* 0 0)" and "(* 1 0)" and "(* 2 0)" and so on infinitely. At least, I think it makes sense. Maybe doing that and relying on rewrite rule scheduling really is the right approach, but it doesn't feel like it.

The problem with the simplification approach is that I don't have an obvious direction for "simpler". One way I was thinking to define it would be to detect rewrites that have variables that don't appear on the RHS, and track when those rewrites get applied. If it applies to my term (+ (+ (* 0 (* x x)) (* 7 x)) 1) then I know I've got another term that I want to rewrite. The downside is that I'm not sure how it interacts with rules like rewrite!("add-self"; "(* ?x 2)" => "(+ ?x ?x)"). I don't see any reason why we couldn't have a situation where every iteration grows a term by doubling it, and in the same iteration a "destructive" rule deletes part of a term made last iteration.

[mwillsey]

I'm still a little bit hung up on "destructive" here. egg rewrites do not destroy any information, as the old left-hand side remains in the e-graph. You don't need a "simpler" directionality; "simpler" is only determined at extraction time.

…

On Mon, May 22, 2023 at 1:03 PM nlewycky ***@***.***> wrote: "Destructive" meaning that the rewrite "destroys information" because the substitution variable on the left isn't present on the right. "(* ?x 0)" to "0" has this property as does "(exp ?x 0)" to "1", but "(+ ?x 0)" to "?x" does not because it's possible to undo the rewrite given the right-hand-side and knowing which rewrite was applied. It makes sense that egg doesn't turn every "0" into "(* 0 0)" and "(* 1 0)" and "(* 2 0)" and so on infinitely. At least, I think it makes sense. Maybe doing that and relying on rewrite rule scheduling really is the right approach, but it doesn't feel like it. The problem with the simplification approach is that I don't have an obvious direction for "simpler". One way I was thinking to define it would be to detect rewrites that have variables that don't appear on the RHS, and track when those rewrites get applied. If it applies to my term (+ (+ (* 0 (* x x)) (* 7 x)) 1) then I know I've got another term that I want to rewrite. The downside is that I'm not sure how it interacts with rules like rewrite!("add-self"; "(* ?x 2)" => "(+ ?x ?x)"). I don't see any reason why we couldn't have a situation where every iteration grows a term by doubling it, and in the same iteration a "destructive" rule deletes part of a term made last iteration. — Reply to this email directly, view it on GitHub <#261 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AANTPTFHRNPKO2QSNGFGRV3XHPA7ZANCNFSM6AAAAAAYHUQMHU> . You are receiving this because you commented.Message ID: ***@***.***>