An e-graph is a data structure, that efficiently stores equivalent terms in a language.
egg [docs]
[blog post]
is a Rust library, that uses e-graphs to build program optimizers and
synthesizers in many domains. To use it, egg::Language
is derived for for your language.
Ruler [paper] uses e-graphs to automatically infer rewrite rules. It generates more minimal rule sets, which improves rewriting speeds, and finds rules that may not have been found manually. It has been used to generate rules for Halide.
Caviar [paper] [CC 2022] is a term-rewriting system for compilers, that improves on the speed of base e-graph TRSs by stopping construction before reaching saturation. It has been used for Halide.
E-graphs have a dedicated workshop at PLDI. The first was EGRAPHS 2022 [video], and it will occur again at PLDI 2023.
Philip Zucker has written notes several posts on e-graphs.
There’s currently much work in connecting Datalog and e-graphs, including:
The Cranelift mid-end has been rearchitected to use acyclic e-graphs (æ-graphs). The design is detailed in the RFC and the doc comment for the initial version. It was rewritten in terms of CLIF data structures in #5382 and enabled by default in version 6.0.0. Chris Fallin will present “ægraphs: Acyclic E-graphs for Efficient Optimization in a Production Compiler” on this work at EGRAPHS 2023.
E-graphs have been discussed several times on the Cranelift Zulip:
Siddharth and Andrés Goens built an egg tactic for Lean.
Philip Zucker was interested in building an e-graph tactic for Coq.
The auto2 tactic in Isabelle/HOL uses e-graphs.
E-graphs are deterministic finite tree automata (DFTAs) [post]. Tree grammars have also been used, for example, to improve parsing, in “Restricting grammars with tree automata” (Michael D. Adams and Matthew Might, 2017).