I’ve always assumed equality saturation is complete for proving equality between terms, until Ryan Wisnesky ask for a proof on Zulip. Turns out simply running equality saturation is not enough! But the good news is, we can get completeness by adding a pretty simple step (just keep enumerating terms and add each one to the e-graph). Proving this works though requires quite a bit of formalism, and I’ll try to lay out the essential parts in this post.
The Problem. Informally, we want to know the following: given a set E of equational axioms and a pair t_1, t_2 of equivalent (according to E) terms, can we prove t_1 = t_2 from the axioms in E? Here both t_1 and t_2 are ground terms. We’ll define exactly what that means in a bit. One example is, given the axioms \forall X, Y: X\times Y = Y\times X, we can prove a \times b = b \times a by setting X = a and Y = b. There is also a more general version of the problem: given a set E of axioms, can we prove another equation e is implied by E? For example, given the axioms: \forall X, Y: X\times Y = Y\times X \forall X, Y, Z: (X\times Y) \times Z = X \times (Y \times Z) we can prove \forall X, Y, Z: (X \times Z) \times Y = X \times (Y \times Z). One important detail is that we only want to prove e if the equality truly holds, and we don’t have to disprove any false equalities. In other words, we want a semi-decision procedure instead of a decision procedure.
Now let’s make the problem statement a bit more formal. Given a vocabulary of function symbols (including constants) \Sigma and a set of variables X, T(\Sigma) denotes the set of expressions constructed from \Sigma, also called ground terms. T(\Sigma, X) denotes the set of expressions constructed from both the function and constant symbols as well as the variables, also called open terms. A model (a.k.a. interpretation) M assigns a value to each constant symbol, and a function to each function symbol. M also comes with a domain of values which is usually implicit. An axiom e = \forall \bar X: \phi(\bar X) holds in an interpretation, written M \models e, if \phi(\bar X) is true for any assignment of \bar X to values in the domain of M, after interpreting each function and constant symbol in \phi according to M. A set E of axioms implies another axiom e, if M \models e for any model such that M \models E (which means all axioms in E hold in M). When e is an equality of the form e = \forall \bar X: t_1 = t_2 (where t_1 and t_2 are open terms over \bar X), we write t_1 =_E t_2 to mean E implies e.
Note that =_E is a semantic relation, because it says that two terms are equal over all interpretations satisfying E. Let’s now consider some syntactic relations that will form the basis of equality saturation. Given an open term t_p (also called a pattern), we say t_p matches another term t if there is a substitution \sigma mapping variables to terms such that \sigma(t_p) is the same as t. Note that t does not need to be ground, and \sigma can also map variables to open terms. A rewrite rule has the form l \rightarrow r where each l and r is an open term. Note that unlike rewrite rules in egg, we don’t require the variables in r to be a subset of that in l. Applying a rewrite rule l \rightarrow to a term t involves first finding a subterm of t that matches l under some substitution \sigma, then replacing that subterm with \sigma(r). We write t \rightarrow_e s if rewriting t with the rule e results in s. t \rightarrow_E s means t \rightarrow_e s for some e \in E. Finally, we write \leftrightarrow_e^* for the reflexive, symmetric, and transitive closure of \rightarrow_E. In other words, t_0 \leftrightarrow_E^* t_k iff there is a sequence t_1, t_2, \ldots, t_{k-1} such that t_i \leftrightarrow_E t_{i+1} for all 0 \leq i < k.
The key result establishing the completeness of equality saturation for equational proofs is Birkhoff’s theorem, which says t_1 =_E t_2 iff t_1 \leftrightarrow_E^* t_2. In English, this says that the terms are equivalent if and only if there is a sequence of rewritings between the terms. As the terms here can be open, the theorem applies to both the ground version and the more general open version of our problem.
At first I thought the completeness of equality saturation directly follows from Birkhoff’s theorem, but that’s actually not true! Consider this example (thanks to Philip Zucker): given the axioms \forall X . f(X) = a and \forall X. f(X) = b, prove a = b. Chugging these into egg won’t work, because the rules can only be applied from left-to-right; to apply either rule from right-to-left, we would have to “guess” some term for X. However, if we just insert a tern f(a) into the e-graph, we succeed: now both rules can be applied to f(a) which rewrites to a and b respectively.
The reason equality saturation failed is that a rewrite rule a la equality saturation is different from the \rightarrow_E relation: in equality saturation, the right-hand-side can only use variables from the left-hand-side. But our “fix” to the example above suggests a general algorithm: equality saturation works as long as the e-graph has enough term to “trigger” the rewrites. To make equality saturation complete (i.e. a semi-decision procedure), we just need to keep enumerating terms from T(\Sigma, X) and insert each one into the e-graph, along side the normal rule applications. This will eventually allow us to construct any finite sequence of rewrites between t_1 and t_2, and by Birkhoff’s theorem proves t_1 =_E t_2.
In this post we have focused on a rather narrow problem, namely checking equalities from a set of equational axioms. Turns out this is a special case of the more general equational logic, where you can have arbitrary first-order sentences over equalities. More precisely, the theory of equational logic with uninterpreted functions is a fragment of FOL where the only predicate is equality (uninterpreted functions and constants are also allowed). This is actually a decidable fragment, and this fantastic paper by Ge & de Moura gives a decision procedure for a generalization of that fragment. The key mechanism in their algorithm is a principled way to do quantifier instantiation, which can be thought of as a smarter way to do our brute-force term enumeration by only building terms using functions that appear in E and e. Another related work is Guided Equality Saturation, where the user manually insert “magic terms” to help out the rewriting process. As Andrés Goens pointed out, our proof here shows Guided Equality Saturation is not limited to run time improvements but actually extends the proving power of plain equality saturation.
The formalisms I’ve used in this post mostly follow Term Rewriting and All That, with a few small changes: they write \stackrel{*}{\leftrightarrow}_E instead of \leftrightarrow^*_E and \approx_E instead of =_E which are a bit harder to type.