Associative/list nodes for SymbolLang

[MostAwesomeDude]

It would be very nice if SymbolLang's patterns supported nodes with varying arity, which represent associative operators in the abstract syntax. It would remove the need for rules which re-associate parentheses, and make peephole optimizers a little simpler.

I imagine that the main reason to not bother doing this is that it has roughly the same computational cost as explicit parenthesis management rules.

[mwillsey]

This would definitely make the users life easier, but it makes the e-matcher's life much harder. Consider you have a bunch of pluses somewhere in the egraph: (+ 1 (+ 2 (+ 3 4))). What if your pattern is (+ ?a ?b)? That should match in many places in that term. In fact, some of the place it matches aren't in the e-graph; consider (+ 2 3)! So what's the root location of those matches? Which e-class is the applier supposed to union it's stuff with?

I totally agree that this is a great feature, but baking in associativity is hard. It turns E-matching into AE-matching (A=associativity, E=equality). People have also done research on ACE-matching (C=commutativity). My current understanding is that these are really hard, but I'd love it if we could figure them out in an efficient way!

[0x0f0f0f]

Hi @mwillsey ! Have you seen the approach proposed in SymbolicUtils.jl? It's classical rewriting, but the solution is interesting.

Quoting from the docs:
Given an expression f(x, f(y, z, u), v, w), an operation f is said to be associative if the expression is equivalent to f(x, y, z, u, v, w) and commutative if the order of arguments does not matter. SymbolicUtils has a special @acrule macro meant for rules on functions which are associate and commutative such as addition and multiplication of real and complex numbers.

@syms x y z

acr = @acrule((~a)^(~x) * (~a)^(~y) => (~a)^(~x + ~y))

acr(x^y * x^z)

Results in x^(y + z)

The pattern matcher tries to match patterns with associative-commutative operations on associative-commutative nodes by either trying to match on all the combinations or permutations of the arguments in the case it's only associative or associative-commutative. Probably distributivity would blow this up in e-graphs, as in SymbolicUtils.jl distributivity is canonicalized when constructing the terms. To currently rewrite SymbolicUtils.jl expressions with my pure-Julia implementation of egg, Metatheory.jl, i just binarize the associative-commutative expressions and then provide explicit assoc-commut-distrib. as rewrite rules, as we also do in egg.

https://github.com/JuliaSymbolics/SymbolicUtils.jl/blob/master/src/rule.jl

Porting a similar approach e-graphs would involve having associative-commutative-distributive e-nodes i guess. Not an easy job, do you think it is possible?s

[mwillsey]

I'll never say never, but ACE-matching is definitely harder than just E-matching (which is already hard!). Furthermore, you have to decide whether to instantiate partial matches. Here's a contrived example: (+ 1 2 3 ... -1 -2 -3 ....). You probably have a rewrite like (+ x -x) -> 0, but there are n ways to apply that here. Do you do all of them simultaneously? Or do you make n separate "splits" of that e-node? I am not sure of the right answers here.

[MostAwesomeDude]

This all makes sense. For posterity, my current solution is to explicitly add associativity with rules, and rely on the egg scheduler to not waste too much time with them. Specifically, in this collection of rules, I have these:

    // associative!
    rw!("comp-assoc-left"; "(comp ?x (comp ?y ?z))" => "(comp (comp ?x ?y) ?z)"),
    rw!("comp-assoc-right"; "(comp (comp ?x ?y) ?z)" => "(comp ?x (comp ?y ?z))"),

And it works well enough so far.