E-graph

Last updated October 31, 2024

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

Definition and operations

Let $\Sigma$ be a set of uninterpreted functions, where $\Sigma _{n}$ is the subset of $\Sigma$ consisting of functions of arity $n$ . Let $\mathbb {id}$ be a countable set of opaque identifiers that may be compared for equality, called e-class IDs. The application of $f\in \Sigma _{n}$ to e-class IDs $i_{1},i_{2},\ldots ,i_{n}\in \mathbb {id}$ is denoted $f(i_{1},i_{2},\ldots ,i_{n})$ and called an e-node.

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

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

Invariants

In addition to the above structure, a valid e-graph conforms to several data structure invariants.^[2] 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 $f(i_{1},\ldots ,i_{n}),f(j_{1},\ldots ,j_{n})$ are congruent when $\mathrm {find} (U,i_{k})=\mathrm {find} (U,j_{k}),k\in \{1,\ldots ,n\}$ . The hashcons invariant states that the hashcons maps canonical e-nodes to their e-class ID.

Operations

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

Equivalent formulations

An e-graph can also be formulated as a bipartite graph $G=(N\uplus \mathrm {id} ,E)$ where

$\mathrm {id}$ is the set of e-class IDs (as above),
$N$ is the set of e-nodes, and
$E\subseteq (\mathrm {id} \times N)\cup (N\times \mathrm {id} )$ is a set of directed edges.

There is a directed edge from each e-class to each of its members, and from each e-node to each of its children.^[3]

E-matching

Let $V$ be a set of variables and let $\mathrm {Term} (\Sigma ,V)$ 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, $\mathrm {Term} (\Sigma ,V)$ is the smallest set such that $V\subset \mathrm {Term} (\Sigma ,V)$ , $\Sigma _{0}\subset \mathrm {Term} (\Sigma ,V)$ , and when $x_{1},\ldots ,x_{n}\in \mathrm {Term} (\Sigma ,V)$ and $f\in \Sigma _{n}$ , then $f(x_{1},\ldots ,x_{n})\in \mathrm {Term} (\Sigma ,V)$ . A term containing variables is called a pattern, a term without variables is called ground.

An e-graph $E$ represents a ground term $t\in \mathrm {Term} (\Sigma ,\emptyset )$ if one of its e-classes represents $t$ . An e-class $C$ represents $t$ if some e-node $f(i_{1},\ldots ,i_{n})\in C$ does. An e-node $f(i_{1},\ldots ,i_{n})\in C$ represents a term $g(j_{1},\ldots ,j_{n})$ if $f=g$ and each e-class $M[i_{k}]$ represents the term $j_{k}$ ( $k$ in $1,\ldots ,n$ ).

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

Extraction

Given an e-class and a cost function that maps each function symbol in $\Sigma$ to a natural number, the extraction problem is to find a ground term with minimal total cost that is represented by the given e-class. This problem is NP-hard.^[7] There is also no constant-factor approximation algorithm for this problem, which can be shown by reduction from the set cover problem. However, for graphs with bounded treewidth, there is a linear-time, fixed-parameter tractable algorithm.^[8]

Complexity

An e-graph with n equalities can be constructed in O(n log n) time.^[9]

Equality saturation

Equality saturation is a technique for building optimizing compilers using e-graphs.^[10] 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 ^[11] 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.^[12] 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.^[13] E-graphs are also used in the Simplify theorem prover of ESC/Java.^[14]

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

E-graphs have been applied to several problems in program analysis, including fuzzing,^[19] abstract interpretation,^[20] and library learning.^[21]

Related Research Articles

<span class="mw-page-title-main">Multivariate normal distribution</span> Generalization of the one-dimensional normal distribution to higher dimensions

In probability theory and statistics, the multivariate normal distribution, multivariate Gaussian distribution, or joint normal distribution is a generalization of the one-dimensional (univariate) normal distribution to higher dimensions. One definition is that a random vector is said to be k-variate normally distributed if every linear combination of its k components has a univariate normal distribution. Its importance derives mainly from the multivariate central limit theorem. The multivariate normal distribution is often used to describe, at least approximately, any set of (possibly) correlated real-valued random variables, each of which clusters around a mean value.

In mathematics, particularly in functional analysis, the spectrum of a bounded linear operator is a generalisation of the set of eigenvalues of a matrix. Specifically, a complex number $is said to be in the spectrum of a bounded linear operator if$

In mathematics, the determinant of an m-by-m skew-symmetric matrix can always be written as the square of a polynomial in the matrix entries, a polynomial with integer coefficients that only depends on m. When m is odd, the polynomial is zero, and when m is even, it is a nonzero polynomial of degree m/2, and is unique up to multiplication by ±1. The convention on skew-symmetric tridiagonal matrices, given below in the examples, then determines one specific polynomial, called the Pfaffian polynomial. The value of this polynomial, when applied to the entries of a skew-symmetric matrix, is called the Pfaffian of that matrix. The term Pfaffian was introduced by Cayley, who indirectly named them after Johann Friedrich Pfaff.

In differential topology, the jet bundle is a certain construction that makes a new smooth fiber bundle out of a given smooth fiber bundle. It makes it possible to write differential equations on sections of a fiber bundle in an invariant form. Jets may also be seen as the coordinate free versions of Taylor expansions.

In mathematics, specifically the algebraic theory of fields, a normal basis is a special kind of basis for Galois extensions of finite degree, characterised as forming a single orbit for the Galois group. The normal basis theorem states that any finite Galois extension of fields has a normal basis. In algebraic number theory, the study of the more refined question of the existence of a normal integral basis is part of Galois module theory.

In mathematics, the tautological one-form is a special 1-form defined on the cotangent bundle $of a manifold In physics, it is used to create a correspondence between the velocity of a point in a mechanical system and its momentum, thus providing a bridge between Lagrangian mechanics and Hamiltonian mechanics.$

String diagrams are a formal graphical language for representing morphisms in monoidal categories, or more generally 2-cells in 2-categories. They are a prominent tool in applied category theory. When interpreted in the monoidal category of vector spaces and linear maps with the tensor product, string diagrams are called tensor networks or Penrose graphical notation. This has led to the development of categorical quantum mechanics where the axioms of quantum theory are expressed in the language of monoidal categories.

In algebraic topology the cap product is a method of adjoining a chain of degree p with a cochain of degree q, such that q ≤ p, to form a composite chain of degree p − q. It was introduced by Eduard Čech in 1936, and independently by Hassler Whitney in 1938.

In quantum information theory, quantum relative entropy is a measure of distinguishability between two quantum states. It is the quantum mechanical analog of relative entropy.

Assortativity, or assortative mixing, is a preference for a network's nodes to attach to others that are similar in some way. Though the specific measure of similarity may vary, network theorists often examine assortativity in terms of a node's degree. The addition of this characteristic to network models more closely approximates the behaviors of many real world networks.

Stress majorization is an optimization strategy used in multidimensional scaling (MDS) where, for a set of -dimensional data items, a configuration of $points in -dimensional space is sought that minimizes the so-called stress function . Usually is or, i.e. the matrix lists points in or dimensional Euclidean space so that the result may be visualised. The function is a cost or loss function that measures the squared differences between ideal distances and actual distances in r -dimensional space. It is defined as:$

In the mathematical theory of artificial neural networks, universal approximation theorems are theorems of the following form: Given a family of neural networks, for each function $from a certain function space, there exists a sequence of neural networks from the family, such that according to some criterion. That is, the family of neural networks is dense in the function space.$

In computer science, more specifically in automata and formal language theory, nested words are a concept proposed by Alur and Madhusudan as a joint generalization of words, as traditionally used for modelling linearly ordered structures, and of ordered unranked trees, as traditionally used for modelling hierarchical structures. Finite-state acceptors for nested words, so-called nested word automata, then give a more expressive generalization of finite automata on words. The linear encodings of languages accepted by finite nested word automata gives the class of visibly pushdown languages. The latter language class lies properly between the regular languages and the deterministic context-free languages. Since their introduction in 2004, these concepts have triggered much research in that area.

In the geometry of numbers, the Klein polyhedron, named after Felix Klein, is used to generalize the concept of continued fractions to higher dimensions.

Network coding has been shown to optimally use bandwidth in a network, maximizing information flow but the scheme is very inherently vulnerable to pollution attacks by malicious nodes in the network. A node injecting garbage can quickly affect many receivers. The pollution of network packets spreads quickly since the output of honest node is corrupted if at least one of the incoming packets is corrupted.

In mathematics, the Lindström–Gessel–Viennot lemma provides a way to count the number of tuples of non-intersecting lattice paths, or, more generally, paths on a directed graph. It was proved by Gessel–Viennot in 1985, based on previous work of Lindström published in 1973.

The generalized distributive law (GDL) is a generalization of the distributive property which gives rise to a general message passing algorithm. It is a synthesis of the work of many authors in the information theory, digital communications, signal processing, statistics, and artificial intelligence communities. The law and algorithm were introduced in a semi-tutorial by Srinivas M. Aji and Robert J. McEliece with the same title.

In discrete mathematics, the Bregman–Minc inequality, or Bregman's theorem, allows one to estimate the permanent of a binary matrix via its row or column sums. The inequality was conjectured in 1963 by Henryk Minc and first proved in 1973 by Lev M. Bregman. Further entropy-based proofs have been given by Alexander Schrijver and Jaikumar Radhakrishnan. The Bregman–Minc inequality is used, for example, in graph theory to obtain upper bounds for the number of perfect matchings in a bipartite graph.

The unique homomorphic extension theorem is a result in mathematical logic which formalizes the intuition that the truth or falsity of a statement can be deduced from the truth values of its parts.

Flag algebras are an important computational tool in the field of graph theory which have a wide range of applications in homomorphism density and related topics. Roughly, they formalize the notion of adding and multiplying homomorphism densities and set up a framework to solve graph homomorphism inequalities with computers by reducing them to semidefinite programming problems. Originally introduced by Alexander Razborov in a 2007 paper, the method has since come to solve numerous difficult, previously unresolved graph theoretic questions. These include the $question regarding the region of feasible edge density, triangle density pairs and the maximum number of pentagons in triangle free graphs.$

References

↑ ( Willsey et al. 2021 )
↑ ( Willsey et al. 2021 )
↑ ( Goharshady, Lam & Parreaux 2024 )
↑ ( de Moura & Bjørner 2007 )
↑ Moskal, Michał; Łopuszański, Jakub; Kiniry, Joseph R. (2008-05-06). "E-matching for Fun and Profit". Electronic Notes in Theoretical Computer Science. Proceedings of the 5th International Workshop on Satisfiability Modulo Theories (SMT 2007). 198 (2): 19–35. doi: 10.1016/j.entcs.2008.04.078 . ISSN 1571-0661.
↑ Zhang, Yihong; Wang, Yisu Remy; Willsey, Max; Tatlock, Zachary (2022-01-12). "Relational e-matching". Proceedings of the ACM on Programming Languages. 6 (POPL): 35:1–35:22. doi: 10.1145/3498696 . S2CID 236924583.
↑ Stepp, Michael Benjamin (2011). Equality saturation: engineering challenges and applications (PhD thesis). USA: University of California at San Diego. ISBN 978-1-267-03827-2.
↑ ( Goharshady, Lam & Parreaux 2024 )
↑ ( Flatt et al. 2022 , p. 2)
↑ ( Tate et al. 2009 )
↑ de Moura, Leonardo; Bjørner, Nikolaj (2008). "Z3: An Efficient SMT Solver". In Ramakrishnan, C. R.; Rehof, Jakob (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 4963. Berlin, Heidelberg: Springer. pp. 337–340. doi: 10.1007/978-3-540-78800-3_24 . ISBN 978-3-540-78800-3.
↑ Rümmer, Philipp (2012). "E-Matching with Free Variables". In Bjørner, Nikolaj; Voronkov, Andrei (eds.). Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings. 18th International Conference, LPAR-18, Merida, Venezuela, March 11–15, 2012. Lecture Notes in Computer Science. Vol. 7180. Berlin, Heidelberg: Springer. pp. 359–374. doi:10.1007/978-3-642-28717-6_28. ISBN 978-3-642-28717-6.
↑ ( Flatt et al. 2022 , p. 2)
↑ Detlefs, David; Nelson, Greg; Saxe, James B. (May 2005). "Simplify: a theorem prover for program checking". Journal of the ACM. 52 (3): 365–473. doi:10.1145/1066100.1066102. ISSN 0004-5411. S2CID 9613854.
↑ Joshi, Rajeev; Nelson, Greg; Randall, Keith (2002-05-17). "Denali: a goal-directed superoptimizer". ACM SIGPLAN Notices. 37 (5): 304–314. doi:10.1145/543552.512566. ISSN 0362-1340.
↑ Yang, Yichen; Phothilimtha, Phitchaya Mangpo; Wang, Yisu Remy; Willsey, Max; Roy, Sudip; Pienaar, Jacques (2021-03-17). "Equality Saturation for Tensor Graph Superoptimization". arXiv: 2101.01332 [cs.AI].
↑ Wang, Yisu Remy; Hutchison, Shana; Leang, Jonathan; Howe, Bill; Suciu, Dan (2020-12-22). "SPORES: Sum-Product Optimization via Relational Equality Saturation for Large Scale Linear Algebra". arXiv: 2002.07951 [cs.DB].
↑ Stepp, Michael; Tate, Ross; Lerner, Sorin (2011). "Equality-Based Translation Validator for LLVM". In Gopalakrishnan, Ganesh; Qadeer, Shaz (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 6806. Berlin, Heidelberg: Springer. pp. 737–742. doi: 10.1007/978-3-642-22110-1_59 . ISBN 978-3-642-22110-1.
↑ "Wasm-mutate: Fuzzing WebAssembly Compilers with E-Graphs (EGRAPHS 2022) - PLDI 2022". pldi22.sigplan.org. Retrieved 2023-02-03.
↑ Coward, Samuel; Constantinides, George A.; Drane, Theo (2022-03-17). "Abstract Interpretation on E-Graphs". arXiv: 2203.09191 [cs.LO].
Coward, Samuel; Constantinides, George A.; Drane, Theo (2022-05-30). "Combining E-Graphs with Abstract Interpretation". arXiv: 2205.14989 [cs.DS].
↑ Cao, David; Kunkel, Rose; Nandi, Chandrakana; Willsey, Max; Tatlock, Zachary; Polikarpova, Nadia (2023-01-09). "babble: Learning Better Abstractions with E-Graphs and Anti-Unification". Proceedings of the ACM on Programming Languages. 7 (POPL): 396–424. arXiv: 2212.04596 . doi:10.1145/3571207. ISSN 2475-1421. S2CID 254536022.

de Moura, Leonardo; Bjørner, Nikolaj (2007). "Efficient E-Matching for SMT Solvers". In Pfenning, Frank (ed.). Automated Deduction – CADE-21. Lecture Notes in Computer Science. Vol. 4603. Berlin, Heidelberg: Springer. pp. 183–198. doi:10.1007/978-3-540-73595-3_13. ISBN 978-3-540-73595-3.
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. arXiv: 2004.03082 . doi:10.1145/3434304. S2CID 226282597.
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. S2CID 2138086.
Flatt, Oliver; Coward, Samuel; Willsey, Max; Tatlock, Zachary; Panchekha, Pavel (October 2022). "Small Proofs from Congruence Closure". In A. Griggio; N. Rungta (eds.). 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. S2CID 252118847.
Goharshady, Amir Kafshdar; Lam, Chun Kit; Parreaux, Lionel (2024-10-08). "Fast and Optimal Extraction for Sparse Equality Graphs". Proceedings of the ACM on Programming Languages. 8 (OOPSLA2): 361:2551–361:2577. doi:10.1145/3689801.

External links

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[1] ( Willsey et al. 2021 )

[2] ( Willsey et al. 2021 )

[3] ( Goharshady, Lam & Parreaux 2024 )

[4] ( de Moura & Bjørner 2007 )

[5] Moskal, Michał; Łopuszański, Jakub; Kiniry, Joseph R. (2008-05-06). "E-matching for Fun and Profit". Electronic Notes in Theoretical Computer Science. Proceedings of the 5th International Workshop on Satisfiability Modulo Theories (SMT 2007). 198 (2): 19–35. doi: 10.1016/j.entcs.2008.04.078 . ISSN 1571-0661.

[6] Zhang, Yihong; Wang, Yisu Remy; Willsey, Max; Tatlock, Zachary (2022-01-12). "Relational e-matching". Proceedings of the ACM on Programming Languages. 6 (POPL): 35:1–35:22. doi: 10.1145/3498696 . S2CID 236924583.

[7] Stepp, Michael Benjamin (2011). Equality saturation: engineering challenges and applications (PhD thesis). USA: University of California at San Diego. ISBN 978-1-267-03827-2.

[8] ( Goharshady, Lam & Parreaux 2024 )

[9] ( Flatt et al. 2022 , p. 2)

[10] ( Tate et al. 2009 )

[11] Moura, Leonardo; Bjørner, Nikolaj (2008). "Z3: An Efficient SMT Solver". In Ramakrishnan, C. R.; Rehof, Jakob (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 4963. Berlin, Heidelberg: Springer. pp. 337–340. doi: 10.1007/978-3-540-78800-3_24 . ISBN 978-3-540-78800-3.

[12] Rümmer, Philipp (2012). "E-Matching with Free Variables". In Bjørner, Nikolaj; Voronkov, Andrei (eds.). Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings. 18th International Conference, LPAR-18, Merida, Venezuela, March 11–15, 2012. Lecture Notes in Computer Science. Vol. 7180. Berlin, Heidelberg: Springer. pp. 359–374. doi:10.1007/978-3-642-28717-6_28. ISBN 978-3-642-28717-6.

[13] ( Flatt et al. 2022 , p. 2)

[14] Detlefs, David; Nelson, Greg; Saxe, James B. (May 2005). "Simplify: a theorem prover for program checking". Journal of the ACM. 52 (3): 365–473. doi:10.1145/1066100.1066102. ISSN 0004-5411. S2CID 9613854.

[15] Joshi, Rajeev; Nelson, Greg; Randall, Keith (2002-05-17). "Denali: a goal-directed superoptimizer". ACM SIGPLAN Notices. 37 (5): 304–314. doi:10.1145/543552.512566. ISSN 0362-1340.

[16] Yang, Yichen; Phothilimtha, Phitchaya Mangpo; Wang, Yisu Remy; Willsey, Max; Roy, Sudip; Pienaar, Jacques (2021-03-17). "Equality Saturation for Tensor Graph Superoptimization". arXiv: 2101.01332 [cs.AI].

[17] Wang, Yisu Remy; Hutchison, Shana; Leang, Jonathan; Howe, Bill; Suciu, Dan (2020-12-22). "SPORES: Sum-Product Optimization via Relational Equality Saturation for Large Scale Linear Algebra". arXiv: 2002.07951 [cs.DB].

[18] Stepp, Michael; Tate, Ross; Lerner, Sorin (2011). "Equality-Based Translation Validator for LLVM". In Gopalakrishnan, Ganesh; Qadeer, Shaz (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 6806. Berlin, Heidelberg: Springer. pp. 737–742. doi: 10.1007/978-3-642-22110-1_59 . ISBN 978-3-642-22110-1.

[19] "Wasm-mutate: Fuzzing WebAssembly Compilers with E-Graphs (EGRAPHS 2022) - PLDI 2022". pldi22.sigplan.org. Retrieved 2023-02-03.

[20] Coward, Samuel; Constantinides, George A.; Drane, Theo (2022-03-17). "Abstract Interpretation on E-Graphs". arXiv: 2203.09191 [cs.LO].
Coward, Samuel; Constantinides, George A.; Drane, Theo (2022-05-30). "Combining E-Graphs with Abstract Interpretation". arXiv: 2205.14989 [cs.DS].

[21] Cao, David; Kunkel, Rose; Nandi, Chandrakana; Willsey, Max; Tatlock, Zachary; Polikarpova, Nadia (2023-01-09). "babble: Learning Better Abstractions with E-Graphs and Anti-Unification". Proceedings of the ACM on Programming Languages. 7 (POPL): 396–424. arXiv: 2212.04596 . doi:10.1145/3571207. ISSN 2475-1421. S2CID 254536022.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]