The Theoretical Aspect of Equality Saturation (Part II)

In the last post, we showed the connections between chase and techniques developed in databases literature and tree automata literature, and how these connections help us understand equality saturation (EqSat). In this blog post, we will focus on a specific problem EqSat faces: the termination problem¹, something my collaborators and I have been working on recently.

The termination problem of EqSat is as follows:

• Instance: a set of rewrite rules \(R\), a term \(t\).
• Problem: does EqSat terminate over \(R\) and \(t\)?

The termination problems of the chase, term rewriting, and tree automata completion, which are defined similarly, have been extensively studied in their respective communities. There are tons of papers on when the chase terminates, when term rewriting terminates, and the problem when tree automata completion terminates is as old as tree automata completion, if not older. This makes sense as in these settings, termination is highly desirable. These algorithms rely on termination to work, and non-termination means no output can be obtained. Unfortunately, the termination problem of tree automata (TA) completion and the chase are both undecidable. Both communities came up with numerous conditions when the problems are decidable.

Compared to TA completion and the chase, the termination problem of EqSat is less disastrous. Equality saturation does not rely on termination for it to be sound: it is always possible to terminate after a fixed number of iterations and yield a partial output. The partial output is still useful in domains where equality saturation is applied, such as program optimization and program verification.

However, if we want stronger guarantees from equality saturation, it is still necessary to ensure EqSat terminates. For example, we can guarantee optimality in program optimization if EqSat saturates in a finite number of steps, at which stage all possible programs have been contained in the output E-graph. Similarly, in program verification, termination also implies decidability of program equivalence checking.

As one may expect, the termination problem of EqSat is not trivial. The undecidability of the termination problem can be shown by a reduction from the halting problem of Turing machines. Fortunately, it is possible to leverage decades of research done on the termination of the above-mentioned techniques like TA completion and the chase, and adapt them to the setting of EqSat. This is an active research topic that we are working on.

One may also wonder what the relationships among the termination problems of EqSat, the chase, term rewriting, and TA completion are. It is possible to reduce the termination of EqSat to the chase via a straightforward encoding. As a result, some techniques on showing chase termination also apply to showing EqSat termination, although the specifics of EqSat are unique enough to make the study on EqSat termination worth exploring. On the other hand, there are examples where EqSat terminates, but term rewriting and TA completion do not, and vice versa.

In conclusion, the termination problem is cool, and I am very excited about the project my collaborators and I are working on. To conclude this blog post, let me present to you some fun exercises:

Do the following rulesets² always terminate in equality saturation for arbitrary E-graphs? Prove your claim.

1. \(\{ f(x)\rightarrow f(g(x)) \}\).
2. \(\{ f(g(x)) \rightarrow f(x) \}\).
3. \(\{ f(g(x)) \rightarrow g(f(x)) \}\).
4. \(\{ f(x, f(y, z)) \rightarrow f(f(x, y), z) \}\).
5. \(\{ f(g(x, y), g(y, z)) \rightarrow g(x, z) \}\).
6. \(\{ f(g(x, y), g(y, z)) \rightarrow g(h(), z) \}\).
7. \(\{ f(f(x, y), z) \rightarrow f(f(x, y), f(f(x, y), z)) \}\).
8. \(\{ h(f(x), y) \rightarrow h(x, g(y)), h(x, g(y)) \rightarrow h(x, y), f(x) \rightarrow x \}\).
9. \(\{ f(x) \rightarrow g(f(h(x))) \}\).
10. \(\{ f(x) \rightarrow g(f(h(x))), h(x) \rightarrow b \}\).
11. \(\{ f(f(x, y), z) \rightarrow g(f(x, z))\}\).
12. \(\{ f(f(x, y), z) \rightarrow g(f(y, x), z) \}\).
13. \(\{ g(f(x, y), z) \rightarrow h(g(x, y), z) \}\).
14. \(\{ f(g(x, y), g(z, x)) \rightarrow g(y, f(x, z)) \}\).

The solutions to these problems are at the end of the blog post :)

¹ I also wrote down some notes on two other problems on equality saturation that I am excited about: extraction and scheduling.

² In this blog post, we assume \(x,y,z\) are variables, \(f,g,h\) are function symbols, and \(a,b,c\) are constants (i.e., nullary functions)

Appendix: Solutions to the Exercise

Do the following rulesets always terminate in equality saturation for arbitrary E-graphs? Prove your claim.

1. \(\{ f(x)\rightarrow f(g(x)) \}\).

   N: Consider an E-graph representing \(f(a)\). Applying this ruleset to it would produce \(f(g(a)), f(g(g(a))),\cdots\), where \(g(a)\not\approx g(g(a))\not\approx \cdots\). If equality saturation terminates, it has to produce infinitely many equivalence classes, which is impossible.

   Visualization for running three iterations:

   

2. \(\{ f(g(x)) \rightarrow f(x) \}\).

   Y: This ruleset always terminates because applying the rule does not create any new E-class. There are only finitely many E-graphs with a bounded number of E-classes. Therefore, equality saturation would always terminate.

3. \(\{ f(g(x)) \rightarrow g(f(x)) \}\).

   N: To prove this does not terminate, let us first introduce a lemma: given a set of rewrite rules \(R\) and an initial E-graph \(G\), \(\rightarrow^*_R(L(G))\subseteq L(\textsf{EqSat}(G, R))\subseteq \leftrightarrow^*_R(L(G))\), where \(\rightarrow^*_R(L(G))\) is the set of terms reachable by terms in \(L(G)\) via \(R\) and \(\leftrightarrow^*_R(L(G))\) is the set of terms equivalent to terms in \(L(G)\) via \(R\).

   Now back to this ruleset. Since we are only working with unary functions in this ruleset, it is more convenient to view it as a string rewriting system \(\{fg\rightarrow gf\}\). Now, consider an initial regular string language \(L=(fg)^*\). Both the reachable terms and equivalent terms of \(L\) under this rewriting system are the set of strings in \((f|g)^*\) with the same number of character \(f\) and character \(g\). This set is not regular (not even context-free), and therefore cannot be represented by a finite E-graph.

4. \(\{ f(f(x, y), z) \rightarrow f(x, f(y, z))\}\).

   N: Consider an E-graph representing identity \(+(a, 0)\approx 0\). This E-graph represents terms \(a, a+0, (a+0)+0, \cdots\). Applying the ruleset to this E-graph would produce subterms \(0+0, (0+0)+0, \cdots\). Moreover, each term is in its own equivalence class, thus an infinite number of E-classes, which is impossible.

5. \(\{ f(g(x, y), g(y, z)) \rightarrow g(x, z) \}\).

   Y: Same as 2, since this ruleset does not produce any new E-class.

6. \(\{ f(g(x, y), g(y, z)) \rightarrow g(h(), z) \}\).

   Y: Applying this ruleset does not produce any new E-class besides \(h()\), so equality saturation always terminates.

7. \(\{ f(f(x, y), z) \rightarrow f(f(x, y), f(f(x, y), z)) \}\).

   Y: This ruleset does not produce any new E-class: any subterm on the right-hand side besides the top level also occurs on the left-hand side.

8. \(\{ h(f(x), y) \rightarrow h(x, g(y)), h(x, g(y)) \rightarrow h(x, y), f(x) \rightarrow x \}\).

   N: It is tempting to think equality saturation would terminate on this ruleset, since this ruleset is convergent. However, equality saturation does not. Consider the following e-graph containing term \(\{ g(a, b)\}\) and identity \(f(a)\approx a\).

   

   Applying the rule \(h(f(x), y)\rightarrow h(x, g(y))\) would “unfold” the left-child E-class that contains \(\{a, f(a), \ldots\}\) and populate \(\{g(b), g^2(b),\ldots\}\) that are pairwise in-equivalent to each other. Since other rules in this rewriting system would not union any of the \(g^n(b)\) with \(g^m(b)\), the E-graph would contain an infinite number of E-classes, which is impossible.

   Not that this ruleset can be “repaired” by adding the rule \(g(b)\rightarrow b\). In other words, we can force termination by contriving additional identities

9. \(\{ f(x) \rightarrow g(f(h(x))) \}\).

   N: Consider an initial E-graph representing \(f(a)\). Equality saturation would populate \(\{g^n(f(h^n(x)))\mid n\in \mathbb{N} \}\), which is not a regular language.

   Visualization for running equality saturation three times:

   

10. \(\{ f(x) \rightarrow g(f(h(x))), h(x) \rightarrow b \}\).

    Y: We can assume the rule \(h(x)\rightarrow b\) is always first applied to the input E-graph and reduce the problem to whether \(\{f(x)\rightarrow g(f(b))\}\) always terminates in equality saturation. It is since the right-hand side is a ground term (term without a variable).

    Note that, in term rewriting, starting with term \(f(b)\), the set of reachable terms form the language \(\{ g^n(f(h^m(x)))\}\mid n,m\in\mathcal{N}, n\geq m\), which is not regular, so no finite E-graph can represent this language. Despite that, equality saturation indeed terminates for this ruleset, because it over-approximates the set of reachable terms.

11. \(\{ f(f(x, y), z) \rightarrow g(f(x, z))\}\).

    Y: This (and the following rulesets) are the tricky ones. This ruleset is “weakly acyclic”. Weak acyclicity is a criterion developed for when the chase terminates, and we can adapt it to decide whether equality saturation terminates.

    Without referring to weak acyclicity, the intuition for why this ruleset terminates is that, in this ruleset, the first child of \(f\) (i.e., \(x\)) stays as the first child and the second child of \(f\) (i.e., \(y, z\)) stays as the second child, so there are only finitely many \(f\) nodes. As a result, there are only finitely many \(g\) nodes, so the E-graph is finite.

12. \(\{ f(f(x, y), z) \rightarrow g(f(y, x), z) \}\).

    Y: This ruleset is also weakly acyclic. To see the intuition, let us first consider rule \(f(f(x, y), z) \Rightarrow f(y, x)\), where \(\Rightarrow\) means “populate the right-hand side, but do not union it with the left-hand side”. This process always terminates, because \(f(y,x)\), the new node created, would not participate in this rule again as \(x\) or \(y\). In other words, there are only a finite number of candidates for \(x\) and \(y\).

    Once all possible \(f(y,x)\)’s are populated with the above process, we can then apply the original rule, which would not create any new E-class, so it would terminate.

13. \(\{ g(f(x, y), z) \rightarrow h(g(x, y), z) \}\).

    Y: This ruleset is also weakly acyclic. The idea is that possible instantiation of \(g(x, y)\) on the right-hand side is bound by \(f(x, y)\), and after all \(g(x,y)\) have been populated, possible instantiations of the right-hand side is bound by the number of \(g\) nodes.

14. \(\{ f(g(x, y), g(z, x)) \rightarrow g(y, f(x, z)) \}\).

    N: Consider an E-graph containing term \(f(g(a, f(a, a)), g(a, a))\). Denote this term as \(u\), and add identity \(f(u, u) = u\) to the E-graph. This egglog program shows that equality saturation does not terminate on this e-graph.