This was a microblog post at first, but I'm crossposting it for visibility and because I'm not 100% convinced the microblog won't collapse at any moment.

VSAs are an acyclic e-graph rooted at a single e-class

I've thought that VSAs were acyclic e-graphs for a while but I never actually checked the e-graph paper. Now I'm pretty convinced.

This gh thread/short paper discuss some relationship between e-graphs and VSAs, but don't show the actual definition https://github.com/egraphs-good/egg/discussions/104

``````Program := Value
| App { op: Function, children: List[Program] }

-- by FlashMeta etc
VSANode := Leaf { asts: Set[Program] }
| Join { op: Function, children: List[VSANode] }
| Union { children: Set[VSANode] }

-- invariant: all programs represented
by a VSANode are equivalent
-- Leaf: all the children asts must be equivalent
-- Join: inductively all the children are equal,
so it's by operator property
-- Union: also inductive

-- based on the egg paper
-- (https://dl.acm.org/doi/pdf/10.1145/3434304)
-- but I interpreted some stuff
-- because there's a lot of indirection
ENode := Final Program
| Join { op: Function, children: List[EClass] }
EClass := Set[ENode]
EGraph := Set[EClass]``````

So if you observe that each case of an `ENode` can represent a (possibly singleton) set on its own, then you can collapse it into one definition and treat the whole thing as a set. Then, the main difference is that an `EGraph` makes the distinction that a `Union` represents an `EClass` and lets an `EGraph` be a set of e-classes. This definition makes a lot of sense when cycles are allowed, since there's not a certain root.

You could also reuse the `VSANode` definition and let `EGraph := Set[VSANode]`, assuming that your type system can't check that it's acyclic

The indirection i referred to in the egg paper is to do with e-class IDs and sticking stuff in an arena, but for VSAs I just used pointers. In an older version of my interactive-vsa site I actually use the `Rc` address as the id of the html node