E-graph

Short description: Data structure

In computer science, an e-graph is a data structure that stores an equivalence relation over terms of some language.

Definition and operations

Let [math]\displaystyle{ \Sigma }[/math] be a set of uninterpreted functions, where [math]\displaystyle{ \Sigma_n }[/math] is the subset of [math]\displaystyle{ \Sigma }[/math] consisting of functions of arity [math]\displaystyle{ n }[/math]. Let [math]\displaystyle{ \mathbb{id} }[/math] be a countable set of opaque identifiers that may be compared for equality, called e-class IDs. The application of [math]\displaystyle{ f\in\Sigma_n }[/math] to e-class IDs [math]\displaystyle{ i_1, i_2, \ldots, i_n\in\mathbb{id} }[/math] is denoted [math]\displaystyle{ f(i_1, i_2, \ldots, i_n) }[/math] and called an e-node.

The e-graph then represents equivalence classes of e-nodes, using the following data structures:

• A union-find structure [math]\displaystyle{ U }[/math] representing equivalence classes of e-class IDs, with the usual operations [math]\displaystyle{ \mathrm{find} }[/math], [math]\displaystyle{ \mathrm{add} }[/math] and [math]\displaystyle{ \mathrm{merge} }[/math]. An e-class ID [math]\displaystyle{ e }[/math] is canonical if [math]\displaystyle{ \mathrm{find}(U, e) = e }[/math]; an e-node [math]\displaystyle{ f(i_1,\ldots,i_n) }[/math] is canonical if each [math]\displaystyle{ i_j }[/math] is canonical ([math]\displaystyle{ j }[/math] in [math]\displaystyle{ 1,\ldots,n }[/math]).
• An association of e-class IDs with sets of e-nodes, called e-classes. This consists of
  • a hashcons [math]\displaystyle{ H }[/math] (i.e. a mapping) from canonical e-nodes to e-class IDs, and
  • an e-class map [math]\displaystyle{ M }[/math] that maps e-class IDs to e-classes, such that [math]\displaystyle{ M }[/math] maps equivalent IDs to the same set of e-nodes: [math]\displaystyle{ \forall i, j\in\mathbb{id},M[i]=M[j]\Leftrightarrow \mathrm{find}(U,i)=\mathrm{find}(U,j) }[/math]

Invariants

In addition to the above structure, a valid e-graph conforms to several data structure invariants. Two e-nodes are equivalent if they are in the same e-class. The congruence invariant states that an e-graph must ensure that equivalence is closed under congruence, where two e-nodes [math]\displaystyle{ f(i_1,\ldots,i_n),f(j_1,\ldots,j_n) }[/math] are congruent when [math]\displaystyle{ \mathrm{find}(U, i_k)=\mathrm{find}(U, j_k),k\in \{1,\ldots,n\} }[/math]. The hashcons invariant states that the hashcons maps canonical e-nodes to their e-class ID.

Operations

E-graphs expose wrappers around the [math]\displaystyle{ \mathrm{add} }[/math], [math]\displaystyle{ \mathrm{find} }[/math], and [math]\displaystyle{ \mathrm{merge} }[/math] operations from the union-find that preserve the e-graph invariants. The last operation, e-matching, is described below.

E-matching

Let [math]\displaystyle{ V }[/math] be a set of variables and let [math]\displaystyle{ \mathrm{Term}(\Sigma, V) }[/math] be the smallest set that includes the 0-arity function symbols (also called constants), includes the variables, and is closed under application of the function symbols. In other words, [math]\displaystyle{ \mathrm{Term}(\Sigma, V) }[/math] is the smallest set such that [math]\displaystyle{ V\subset\mathrm{Term}(V, \Sigma) }[/math], [math]\displaystyle{ \Sigma_0\subset\mathrm{Term}(\Sigma, V) }[/math], and when [math]\displaystyle{ x_1, \ldots, x_n\in \mathrm{Term}(\Sigma, V) }[/math] and [math]\displaystyle{ f\in\Sigma_n }[/math], then [math]\displaystyle{ f(x_1,\ldots,x_n)\in\mathrm{Term}(\Sigma, V) }[/math]. A term containing variables is called a pattern, a term without variables is called ground.

An e-graph [math]\displaystyle{ E }[/math] represents a ground term [math]\displaystyle{ t\in\mathrm{Term}(\Sigma, \emptyset) }[/math] if one of its e-classes represents [math]\displaystyle{ t }[/math]. An e-class [math]\displaystyle{ C }[/math] represents [math]\displaystyle{ t }[/math] if some e-node [math]\displaystyle{ f(i_1,\ldots,i_n)\in C }[/math] does. An e-node [math]\displaystyle{ f(i_1,\ldots,i_n)\in C }[/math] represents a term [math]\displaystyle{ g(j_1,\ldots,j_n) }[/math] if [math]\displaystyle{ f=g }[/math] and each e-class [math]\displaystyle{ M[i_k] }[/math] represents the term [math]\displaystyle{ j_k }[/math] ([math]\displaystyle{ k }[/math] in [math]\displaystyle{ 1,\ldots,n }[/math]).

e-matching is an operation that takes a pattern [math]\displaystyle{ p\in\mathrm{Term}(\Sigma, V) }[/math] and an e-graph [math]\displaystyle{ E }[/math], and yields all pairs [math]\displaystyle{ (\sigma, C) }[/math] where [math]\displaystyle{ \sigma\subset V\times\mathbb{id} }[/math] is a substitution mapping the variables in [math]\displaystyle{ p }[/math] to e-class IDs and [math]\displaystyle{ C\in\mathbb{id} }[/math] is an e-class ID such that each term [math]\displaystyle{ \sigma(p) }[/math] is represented by [math]\displaystyle{ C }[/math]. There are several known algorithms for e-matching, the relational e-matching algorithm is based on worst-case optimal joins and is worst-case optimal.

Complexity

• An e-graph with n equalities can be constructed in O(n log n) time.

Equality saturation

Equality saturation is a technique for building optimizing compilers using e-graphs. It operates by applying a set of rewrites using e-matching until the e-graph is saturated, a timeout is reached, an e-graph size limit is reached, a fixed number of iterations is exceeded, or some other halting condition is reached. After rewriting, an optimal term is extracted from the e-graph according to some cost function, usually related to AST size or performance considerations.

Applications

E-graphs are used in automated theorem proving. They are a crucial part of modern SMT solvers such as Z3 and CVC4, where they are used to decide the empty theory by computing the congruence closure of a set of equalities, and e-matching is used to instantiate quantifiers. In DPLL(T)-based solvers that use conflict-driven clause learning (also known as non-chronological backtracking), e-graphs are extended to produce proof certificates. E-graphs are also used in the Simplify theorem prover of ESC/Java.

Equality saturation is used in specialized optimizing compilers, e.g. for deep learning and linear algebra. Equality saturation has also been used for translation validation applied to the LLVM toolchain.

E-graphs have been applied to several problems in program analysis, including fuzzing, abstract interpretation, and library learning.

References

• de Moura, Leonardo; Bjørner, Nikolaj (2007). "Efficient E-Matching for SMT Solvers". in Pfenning, Frank (in en). Automated Deduction – CADE-21. Lecture Notes in Computer Science. 4603. Berlin, Heidelberg: Springer. pp. 183–198. doi:10.1007/978-3-540-73595-3_13. ISBN 978-3-540-73595-3. https://link.springer.com/chapter/10.1007/978-3-540-73595-3_13. 
• Willsey, Max; Nandi, Chandrakana; Wang, Yisu Remy; Flatt, Oliver; Tatlock, Zachary; Panchekha, Pavel (2021-01-04). "egg: Fast and extensible equality saturation". Proceedings of the ACM on Programming Languages 5 (POPL): 23:1–23:29. doi:10.1145/3434304. https://doi.org/10.1145/3434304. 
• Tate, Ross; Stepp, Michael; Tatlock, Zachary; Lerner, Sorin (2009-01-21). "Equality saturation". Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL '09. Savannah, GA, USA: Association for Computing Machinery. pp. 264–276. doi:10.1145/1480881.1480915. ISBN 978-1-60558-379-2. https://doi.org/10.1145/1480881.1480915. 
• Flatt, Oliver; Coward, Samuel; Willsey, Max; Tatlock, Zachary; Panchekha, Pavel (October 2022). "Small Proofs from Congruence Closure" (in en). Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022. TU Wien Academic Press. pp. 75–83. doi:10.34727/2022/isbn.978-3-85448-053-2_13. ISBN 978-3-85448-053-2. https://repositum.tuwien.at/handle/20.500.12708/81325. 

External links

• The Egg Project
• A Colab notebook explaining e-graphs