Max Willsey, Chandrakana Nandi, Yisu Remy Wang
Oliver Flatt, Zachary Tatlock, Pavel Panchekha
2020 · arXiv
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a more recent technique known as equality saturation repurposes e-graphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers. However, e-graphs remain unspecialized for this newer use case. Equality saturation workloads exhibit distinct characteristics and often require ad-hoc e-graph extensions to incorporate transformations beyond purely syntactic rewrites. This work contributes two techniques that make e-graphs fast and extensible, specializing them to equality saturation. A new amortized invariant restoration technique called rebuilding takes advantage of equality saturation's distinct workload, providing asymptotic speedups over current techniques in practice. A general mechanism called e-class analyses integrates domain-specific analyses into the e-graph, reducing the need for ad hoc manipulation. We implemented these techniques in a new open-source library called egg. Our case studies on three previously published applications of equality saturation highlight how egg's performance and flexibility enable state-of-the-art results across diverse domains.
Metadata: arXiv. Abstracts retain their original authors’ rights.
Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels
4 selected excerpts · 4 total mentions
I was about to comment that this reminds me of Aaron Hsu’s Dyalog compiler, but it’s mentioned right there in the README as one of the inspirations. IMHO, compilers are about an order of magnitude slower than they could be, and this type of tree representation could be one key element for fixing that. One interesting approach would be to combine egg[1] with this style of vectorised trees for efficient optimisation passes. [1] https://arxiv.org/pdf/2004.03082.pdf
Yes, 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 http://www.philipzucker.com/souffle-egg4/ https://arxiv.org/pdf/2004.03082.pdf
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 to the best of my knowledge. P.S: I'm currently implementing them in Haskell https://github.com/alt-romes/hegg
The author frames this as a contest between two architectures: either spend a lot of effort building custom developer tools, or repurpose the compiler as a server for multiple clients. Both approaches have their tradeoffs: the first, as the author mentions, violates DRY [1]. The second violates the Unix philosophy [2]. However, there is a third way. Both developer tools and compilers can be seen as special cases of a much simpler and more general pattern known as a graph database [3, 4, 5]. [1]: https://en.wikipedia.org/wiki/Don%27t_repeat_yourself [2]: https://en.wikipedia.org/wiki/Unix_philosophy [3]: https://www.youtube.com/watch?v=WxyyJyB_Ssc [4]: https://petevilter.me/post/datalog-typechecking/ [5]: https://arxiv.org/pdf/2004.03082.pdf
More from the same topics.
William P. Thurston
In response to Jaffe and Quinn [math.HO/9307227], the author discusses forms of progress in mathematics that are not captured by formal proofs of theorems, especially in his own work in the theory of foliations and geometrization of 3-manifolds and dynamical systems.
Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan +11
Artificial intelligence (AI) researchers have been developing and refining large language models (LLMs) that exhibit remarkable capabilities across a variety of domains and tasks, challenging our understanding of learning and cognition.
Martin Kleppmann
The CAP Theorem is a frequently cited impossibility result in distributed systems, especially among NoSQL distributed databases.
Eric Chisolm
This is an introduction to geometric algebra, an alternative to traditional vector algebra that expands on it in two ways: 1.