3 ms·
Equality graphs (e-graphs) for theorem proving and equality saturation and other equality-related things. They're awesome data structures that efficiently main
by romes 4y ago
Equality graphs (e-graphs) for theorem proving and equality saturation and other equality-related things.
They're awesome data structures that efficiently maintain a congruence relation over many expressions
> At a high level, e-graphs extend union-find to compactly represent equivalence classes of expressions while maintaining a key invariant: the equivalence relation is closed under congruence.
e.g. If I were to represent "f(x)" and "f(y)" in the e-graph, and then said "x == y" (merged "x" and "y" in the e-graph), then the e-graph, by congruence, would be able to tell me that "f(x) == f(y)"
e.g. If I were to represent "a*(2/2)", in the e-graph, then say "2/2 == 1", and "x*1 == x", by congruence the e-graph would know "a*(2/2) == a" !
The most recent description of e-graphs with an added insight on implementation is https://arxiv.org/pdf/2004.03082.pdf https://arxiv.org/pdf/2004.03082.pdf to the best of my knowledge.
P.S: I'm currently implementing them in Haskell https://github.com/alt-romes/hegg https://github.com/alt-romes/hegg
- FnuGk 4y agoIsnt that the building blocks of logic based programming languages like Prolog?
- Twisol 4y agoI had a similar thought when I learned about e-graphs. I'm not sure yet, but I think congruence closure is a slightly different problem from the one Prolog unification solves. In particular, if you tell an e-graph that `f(x) = g(y)`, it will take you at your word -- while Prolog would give a unification error. (An e-graph should also handle `X = f(X)`, while this would fail Prolog's admittedly often-ignored occurs check.)
- superlopuh 4y agoYes, at least these egg-based projects are usign this idea, but it looks like it's just one of the options: https://souffle-lang.github.io/docs.html https://souffle-lang.github.io/docs.html http://www.philipzucker.com/souffle-egg4/ http://www.philipzucker.com/souffle-egg4/ https://arxiv.org/pdf/2004.03082.pdf https://arxiv.org/pdf/2004.03082.pdf
- gopiandcode 4y agoShameless plug, I also maintain an OCaml implementation of egraphs (named ego) at https://github.com/verse-lab/ego https://github.com/verse-lab/ego While the most popular implementation at the moment seems to be egg in Rust, I find that OCaml serves as a much more ergonomic environment for quickly prototyping out uses of egraphs in practice. As a bonus, ego also shares the same logical interface as egg itself, so once you've finalised your designs, you shouldn't have much trouble porting them to egg if you need the performance gains.
- smasher164 4y agoI wonder if you could apply e-graphs to situations where the union-find data structure would be used, i.e. if there are any additional benefits gotten from the congruence relation.
- HelloNurse 4y agoMore pointers and more processing in exchange for representing equivalence classes of many, often infinitely many graphs compactly and enumerating them efficiently. Usually not relevant when equivalence of simple nodes is the object.