Why reasonable rules can create infinite loops

[jkoppel]

Why reasonable rules can create infinite loops

Myth: If a set of rewrite rules terminates when applied to all inputs when viewed as a term-rewriting system, then it will also terminate when used in equality saturation / e-graph rewriting.

Fact: A set of terminating rewriting rules may yield an infinite number of distinct e-classes.

---

This post summarizes discussions between myself and several of the egg authors about unexpected loops in equality saturation, along with my own attempts at characterizing the problem using term-rewriting theory.

---

Preamble: Terminology and Background

We introduce some terminology from term-rewriting theory. All of this can be found in either "Term Rewriting and All That" (Baader and Nipkow, 1998) or "Termination of Rewriting" (Dershowitz, 1987).

Terminology

Terminating: A set of rules is terminating if there is no infinite derivation from any start term.
Quasi-terminating: A set of rules is quasi-terminating if every infinite derivation has a cycle
Globally finite: A set of rules is globally finite if the number of distinct terms generated from any start term is finite. For systems with a finite number of rules, this is equivalent to quasi-termination.

Note that the property of interest for equality saturation is distinct from global finiteness: equality saturation terminates not if there are a finite number of distinct (non-equivalent) terms, but if there are a finite number of distinct subterms. For instance, in the infinite sequence of terms {0, a-a, (a+a)+(-a-a), (a+a+a)+(-a-a-a), ...}, every term is equivalent to 0, but there are an infinite number of non-equivalent subterms.

Overlap: Two patterns A and B overlap if B unifies with a (non-variable) subterm of A, or vice versa. See examples below under critical overlap.

Critical overlap: Two rules A => B and C => D have critical overlap if A unifies with a nontrivial subterm of B or vice-versa. For example, the rules f(g(x)) => A and g(h(y)) => B have critical overlap because g(x) unifies with g(h(y)) (with the unifier [x |-> h(y)]). This yields the term f(g(h(y)), which steps to both A and f(B). The rules f(x) => A and g(y) => B do not have critical overlap; while g(y) does unify with x (unifier: [x |-> g(y)]), this unification is trivial. The associativity rule (x+y)+z => x+(y+z) has critical overlap with itself (unifier: [x |-> x + y, y |-> z]), yielding the term after renaming ((w+x)+y)+z, which steps to both (w+x)+(y+z) and (w+(x+y))+z.

Proving Termination

https://en.wikipedia.org/wiki/Rewrite_order

The typical way to prove termination is to find a reduction order <=. If <= is a well-founded partial order and, for any terms t, u with t => u, it must be that u < t, then the rewrite system is terminating.

To show quasi-termination, a thin preorder is used instead of a partial order. A preorder is any transitive relation R; if a R b and b R a, then a and b are in the same equivalence class of R. A thin preorder is a preorder whose equivalence classes are all finite.

Nonterminating Example

The most common problematic example comes from associativity combined with annihilation.

Consider the system with rules (a+b)+c => a+(b+c), a+0 => a, and (-b)+b => 0. It is easy to see this ruleset is terminating as a term-rewriting system because each reduction either reduces the lexicographic ordering (total term size, term size of left child). However, when applied to egraphs, it deduces that a=(a+(-b))+b, and then produces the infinite derivation

(a+(-b))+b
=> a+(-b+b)
= ((a+(-b))+b)+(-b+b)
=> (a+(-b))+(b+(-b+b))
=> a + ((-b)+(b+(-b+b)))
=> ...

For this example, judiciously collapsing all right subterms into the two eclasses of b and 0 prevents blowup. However, merely adding the commutativity rule a+b => b+a (which brings the underlying rewrite system from terminating to quasi-terminating) permits the system to rearrange the arbitrarily-large sum of b's and -b's arbitrarily, resulting in an infinite number of eclasses, and hence causes equality saturation to loop infinitely.

Characterization

Precisely characterizing the situations when e-graph rewriting blows up for a "reasonable" rule-set (or, more generally, characterizing the differences between e-graph and term rewriting) is an unsolved research problem. However, here are some properties of an offending rule system:

Cyclic terms are bad

In the associativity example, the problem came that (a+(-b)+b is equivalent to a subterm of itself, a. Replacing a with the identifier "eclass-1" yields the term eclass-1=<a, (eclass-1+(-b))+b>, which is cyclic, and hence represents arbitrarily (or infinitely) large terms.

More generally, when there is a cyclic term (a term equal to a subterm of itself), rewrite rules which appear not to grow the term can in fact grow the term arbitrarily.

With cyclic terms, there must be a rule whose LHS has depth at least 2

If all rules have an LHS depth of at most 1, then all rewrites will copy an e-class wholesale. For example: the commutativity rule a + b => b + a cannot cause an explosion, as, even if a = a + b (so that the term can be written eclass-1 = <a, eclass-1 + b>), this could merely rewrite eclass-1 + b to b + eclass-1and not forcibly expand eclass-1 to something larger.

A rule whose LHS overlaps its RHS is trouble

The important thing is actually that there is a composition of rules whose final RHS overlaps the initial LHS, but examples are easier to find for a single rule. Associativity satisfies this condition, as one can apply it twice in a row to a term like ((w+x)+y)+z. Commutativity also satisfies this condition, but it is also depth-1 (see above).

Cyclic terms are not necessary

Consider the rule system A => B, f(A, y) => g(B, h(y, y)), g(A, x) => f(A, X). As a term-rewriting system, it is trivial to see this is terminating. However, as an e-graph rewriting system, the start term f(A, B) blows up infinitely. This is because treating it as an e-graph rewriting system effectively adds the rule B => A, which renders the term-rewriting system nonterminating (and non-quasi-terminating).

However, the rule set with associativity is still quasi-terminating, but blows up as an e-graph rewriting system. We conjecture that, if R is a quasi-terminating rewrite system which is symmetric in the sense that, for each rule A => B, a corresponding B => A rule exists, and R is non-terminating as an e-graph rewriting system, then R can generate a cyclic term.

Mitigation

No general solution to the problem of infinite derivations from associativity and similar rules is known. There are different domain-specific solutions based on the premise that most applications do not need to find all equivalent terms (saturation), but can make do with merely finding a large number of them (called "moistening" by Edward Kmett).

Rule scheduling

Egg's default exponential-backoff scheduler ( https://docs.rs/egg/0.6.0/egg/struct.BackoffScheduler.html ) has been found to be effective at mitigating this problem, detecting likely cycles by seeing a rule fire too many times, and then temporarily banning it in favor of other rules.

Early pruning

For an optimization setting, it can be effective to remove members of an eclass which are strictly worse than another member. For example, if an eclass contains both 0 and a*0, then remove the a*0.

Abandon general matching for certain nodes

Chandrakana Nandi writes:

"Speaking of domain specific solutions, in our Szalinski work, we encountered a slightly different flavor of AC-matching due to working with permutations / partitioning of lists. There, we solved the problem by not adding all permutations / partitions in the egraph. Instead we called out to a custom solver to figure out if there is a useful reordering and added just that reordering to the egraph. "

[mwillsey]

Thanks for writing this up Jimmy, these are some keen observations! From egg's perspective, we have indeed targeted those applications where saturation isn't required. We were actually just chatting about potentially finding a name for the technique that conveys that we are using e-graphs for rewriting but don't care about saturation ("moistening" wouldn't be my choice 😄, perhaps just "e-graph rewriting").

What kind of applications require saturation? Even when we've used egg as a theorem prover, it's been for undecidable (first-order) logics.

[remysucre]

For one, a superoptimizer (e.g. Denali) would require saturation to guarantee optimality.

[taktoa]

Isn't the issue with (a+b)+c => a+(b+c), a+0 => a, and (-b)+b => 0 just that equality saturation doesn't actually take an arbitrary TRS as input -- instead, it morally takes a TRS where, for every rule X => Y, there exists a rule Y => X, and when you give it an arbitrary TRS it is just "completing" the TRS to that form. So really, the condition that matters isn't whether the TRS T is terminating, it's whether the completion of T is terminating. Am I right in saying that equality saturation always terminates whenever the completion of the input TRS is terminating, or is there some other situation I'm missing?

[mwillsey]

Just for my own sake, I ran this in egg and it indeed does not saturate.

[remysucre]

I convinced Jimmy that this example should not terminate on the given schedule either. I’ll attempt a formal proof of the independence of termination and order later

[chandrakananandi]

Ok I played around a bit with this ruleset:

R1: h(g(x, Z)) => h(g(f(x), Z))
R2: g(f(x), y) => g(x, f(y))
R3: g(Z, y) => g(Z,Z)

and starting with the term h ( g (Z, Z)), as soon as R1 applies we get: h (g (f (Z), Z)) and then R1 again applies to give:
h (g (f (f (Z)), Z)) and so on. R2 and R3 rewrite terms down to g(Z, Z) but it doesn't stop R1 from continuing to generate the next round of h (g (f (f (f ...))), Z )). So I also agree that this cannot terminate in vanilla equality saturation (I think irrespective of all-at-once / one-at-a-time application, but I am not 100% on that).

If you stop applying R1 completely at some point and only apply R2 and R3 from there on, it will terminate but that is not what @jkoppel is suggesting below:

But, in a rule schedule that runs the two g rules to saturation before the h rules, it will terminate.

R1 is allowed to apply again in your schedule, right?

[chandrakananandi]

What is rule salience in Clara? Is it a way to stop a rule from being applied if some condition is met?

[jkoppel]

R1 is allowed to apply again in your schedule, right?

Yes it is.

What is rule salience in Clara? Is it a way to stop a rule from being applied if some condition is met?

http://www.clara-rules.org/docs/conflictsalience/

"Salience is simply a integer property attached to the rule, where rules with higher values will fire before rules with lower values. Here is a simple example:"

It's a fancy word for "priority," because industry people like making up their own terminology.

I am down to <40% confidence that rule priority affects termination, but still at at least 70% confidence it can have a major effect on running time.

[ekmett]

FWIW- Equality "moistening" was originally coined by @deviant-logic. I just adopted it.

[0x0f0f0f]

Hi! Author of Metatheory.jl (re-implementation and extension of egg in julia). Has anything been done on automatic pruning of an e-graph? Im working in parallel towards smarter automatic schedulers. I guess they are two similar ways of reducing the search space, but orthogonally in regard to eclasses for pruning and to rules for scheduling.

[remysucre]

I tend to avoid pruning except for perhaps constant folding, since pruning goes against the monotone principle of equality saturation and frequently creates subtle bugs