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