E-graphs modulo theories - with applications to associative-commutative operators

Abstract

E-graphs are a data structure for equational theorem proving which provide the basis for equality saturation, a method to automatically derive equational consequences from a starting set of terms, equations, and identities. E-graphs have generated a lot of interest since the publication of the Egg paper by Willsey et al. [23], which describes a fast implementation of E-graphs and its application to a variety of problems. However, E-graphs struggle with a combinatorial explosion when reasoning about certain theories. A notorious case is that of AC theories, those containing associative and commutative operators: the space complexity of saturation is exponential (more precisely, O(3n)) in the size of the input in the worst case. Can equality saturation for AC theories be done in a more efficient way? There have been several proposals for extending E-graphs to E-graphs modulo theories (EMTs) [26, 14, 17]. These proposals suggest integrating a theory-specific reasoning method for AC together with the general mechanisms of E-graphs and equality saturation in order to efficiently deal with AC theories. The hope is that specific methods for AC theories can avoid the inefficiencies in using the general equality saturation mechanism for the AC identities. However, there is a limitation in previous proposals for EMTs for AC, which cause the resulting notion of EMT to be unable to determine straightforward consequences of the AC identities. This thesis develops a notion of EMT that addresses this issue and shows that it is possible to reason with AC theories and a variety of closely related theories in a way that avoids the worst inefficiencies of plain E-graphs. It also provides a formal definition of EMTs that we hope can provide the basis for future work on integrating other theories in a similar manner. Finally, we discuss an implementation of EMTs and benchmark it against pure E-graph reasoning on a variety of equational reasoning tasks (5.3), showing significant space savings compared to ordinary E-graphs. Central to our notion of a ‘good’ theory for an EMT is the necessity of a solver for the word problem over the theory. This gives us a lower bound on EMTs for AC: the word problem for AC requires in the worst case exponential space and doubly-exponential time. This is an improvement over the space upper bound for ordinary E-graphs, but highlights that concrete efficiency gains derive from the potential for typical problems to be solvable efficiently. Our solver for AC and polynomials builds upon Buchberger’s algorithm, on which significant work has been done to achieve good common-case performance. Theories similar to AC, such as those with identities for units, negation, or scalar multiplication, have word problems solvable via Buchberger-like algorithms, and in certain cases, AC-like theories can be solved significantly more than AC by itself. Thus our work provides a foundation for future generalization to a this large family of AC-like theories.