Graph Rewriting with E-Graphs

[cat-state]

Is it possible to represent graph rewriting with e-graphs?
I can understand how to represent regular string and tree based languages, but I'm not sure how one would represent a graph terms within an e-graph.

[mwillsey]

Yes it should be possible, especially with the recent addition of multipatterns. The difficulty is representing DAGs (or even graphs with cycles) in terms outside the e-graph; inside the e-graph should work just fine. For example, you can make a cycle by merging things with a "nonce" term (pseudocode below):

let class = egraph.add(0 + x);
egraph.union(class, x);

[Bastacyclop]

It could be useful if multi-root DAGs were supported by the library APIs, and not just expressions, for example:

• add_expr doesn't work for DAGs, see Add LP extractor #128 (comment)
• as a result, same for explain_equivalence

Although there's always the workaround to collect all roots into one by adding a special node which avoids making the API more complex.

[phannebohm]

Some time ago I read this paper mentioning an algebra of graphs. It's probably not very useful for graphs beyond a certain size, but maybe it's an interesting object of study.