Support regular term rewriting?

[Bastacyclop]

Hi!

I would like to compare greedy rewriting (only apply rewrites that decrease term cost) to equality saturation without having to define the same rewrite rules twice. It could be useful if rewrite rules defined with egg could be also applied to regular terms and not only e-graphs?

I guess for Patterns that should just be a matter of adding some new methods. For Searcher/Applier/Rewrite that might be more tricky, maybe for more advanced constructs I need to define my own rewrite macro/DSL to generate both term rewriting functions and e-graph Rewrites.

[mwillsey]

I agree that that is possible and a good idea in general, but I think there are a lot of API questions that would need to be ironed out. I would categorize this as a "major feature" to be added to egg, so it's on the todo list, but it might take a while.

[Bastacyclop]

I have an experimental branch of egg where I implemented destructive term (and DAG) rewriting: main...Bastacyclop:egg:standard-rewrite
I didn't try to make a nice interface design -- just to get the feature running.
Basically I added my own Graph structure which is a bit like an EGraph without equivalence classes. It reuses the Language trait without issues but does not implement analyses yet. Because it is hash-consed I was able to reuse the existing syntactic rewrite rules and EGraph matching programs as-is, just with a slightly simplified execution code that doesn't have to deal with equivalent e-nodes.
Interestingly I found that mutable replacement in this graph could be achieved with a procedure not that different from the e-graph rebuilding but with some twists and garbage collection. It might also be a better design to avoid mutation and implement a persistent structure instead but it sounded like more work for a quick prototype.
I had to create my own GraphCostFunction trait but better design may get rid of this (or at least provide a common trait compatible with both worlds).

[mwillsey]

Very cool! Although, my understanding in your original post was that you wanted the ability to do destructive rewriting in an e-graph, and this seems to be a different thing.

I think the former is definitely possible, the question is: what you do delete when you perform a destructive rewrite? Just the root e-node that was matched? All matched e-nodes? I think just deleting the top matched e-node should work, but maybe you need to delete more...