The Diamond Lemma
When does a system of simplification rules produce a unique result?
I found this result useful for a few different problems I was thinking about recently. It cleared up a lot of confusion I had around simplification rules. First I give a semiformal statement of the lemma and some applications. At the end I give a formal statement and proof.
Setup
Suppose you have a set S and some possible transitions where one element of S “simplifies” into another. The diamond lemma has two requirements:
There is no infinite chain of simplifications. If you start somewhere and keep simplifying, you will eventually reach a terminal state where no simplifications are possible.
If some state s1 has simplifications to both s2 and s3, then there are paths to “merge” s2 and s3 back to some common state t (see the diagram). This is the “diamond” from the lemma’s name.
If both of these requirements are met, the diamond lemma guarantees that if you start simplifying from a given state s, the final state you end up at is the same, regardless of which path you choose.
Examples
Abelian sandpiles
Let G be a connected graph. Label some vertex t of G as the sink. Each vertex will have some nonnegative number of grains of sand on it. If the number of grains of sand on some vertex v is at least the number of neighboring vertices, you can “topple” that vertex by moving one grain of sand to each neighboring vertex from v. Any grains of sand that move to the sink disappear instead of accumulating.
It turns out that if you start topple from some initial configuration until no further topples are possible, the final state is independent of which topples you choose to make! This fact was pretty surprising to me when I first heard it, but is easy to prove with the diamond lemma.
First we have to show there is no infinite chain. If there was an infinite chain then some vertex would have to fire infinitely many times. Then all of its neighbors also have to fire infinitely many times (to expel the infinite number of grains going into them), but since our graph is connected, every vertex must fire infinitely many times. Some vertex is next to the sink, which means infinitely many grains get dumped into the sink, which is impossible because we only started with finitely many grains.
Next we have to show the diamond property. Suppose that two different vertices u and v can both topple. The states after toppling u and v respectively will be different; we have to find paths to merge them back together. This turns out to be pretty easy. After we topple u, the number of grains on v does not decrease, so v can still topple. Similarly, we can first topple v, then u. The final result is the same, so we have our two sides of the diamond.
Exercises for the reader (Doesn’t use the diamond lemma, just fun results about sandpiles. Hints in rot13.): Fix a graph G and a sink vertex t. Call a sandpile reduced if no topples are possible. Call a sandpile A recurrent if it is reduced and for any integer n, there is some other sandpile B where each non-sink vertex has at least n grains, and B reduces to A. Define an operation + on reduced sandpiles where A+B is calculated by adding the numbers of grains from A and B pointwise, then toppling to a reduced sandpile.
Show that there exist recurrent sandpiles A and E such that A+E=A. (Nqq gur fnzr fnaqcvyr gb vgfrys ercrngrqyl.)
Show that for all recurrent sandpiles B, B+E=B, where E is the sandpile from part 1. (Znxr n fhssvpvragyl ynetr fnaqcvyr gung erqhprf gb O. Gura nqq gur fnzr fnaqcvyr gb obgu fvqrf bs gur rdhngvba va cneg 1.)
Show that the recurrent sandpiles form a group under +.
Show that a sandpile A is recurrent if and only if it is reduced and can be reached from some sandpile B by some sequence of topples where each non-sink vertex is toppled at least once. (Fgnegvat sebz O, nqq bar tenva gb rnpu arvtuobe bs gur fvax. Fubj gung lbh pna gura gnxr gur frdhrapr bs gbccyrf sebz O gb N naq nccraq bar gbccyr ng rnpu iregrk, va beqre bs jura gubfr iregvprf gbccyrq ynfg. Gura fubj lbh pna nqq a tenvaf gb rnpu arvtuobe bs gur fvax. Svanyyl fubj gung guvf yrgf lbh nqq znal tenvaf rireljurer.)
Monoids
If you don’t know what a monoid is, don’t worry. Let’s say we have some strings composed of xs and ys. We can “multiply” these strings together by concatenating them: xyxyy·xy=xyxyyxy. We write 1 for the empty string - multiplying by 1 does nothing. We can use superscripts to represent powers of a string - so (xy)2=xyxy. Let’s say we want to add some relations. Let’s start with the relation x2=1. This means two xs in a row are equivalent to the empty string and we can remove them, so that yxxxyxx can turn in to yxy. We’re also allowed to insert two xs wherever we want into a string without changing the result, sort of like you will sometimes multiply and divide by the same quantity while solving a math problem. If we want to simplify a string, we can just remove adjacent xs wherever they appear. Simple!
Now let’s add another relation. Suppose we want the relation xy=y2x. Let’s say that to simplify we try to bring ys to the front, so let’s say that whenever we see the substring xy, we replace it with yyx. Let’s try simplifying xxy. We can use the first relation to eliminate the xx and simplify to y. However, we could also have used the second relation to simplify to xyyx. This string simplifies again to yyxyx, which turns into yyyyxx, which finally turns into yyyy. These relations imply y4=y, which we can’t get from our simplification rules! To turn y4 into y, we have to apply one of our rules backwards and insert two xs out of nowhere. Is there a set of relations where we can easily see whether or not two strings are equivalent, without having to go in reverse?
Let’s add the new rule we found, so that we have three simplification rules: xx→1, xy→yyx, and yyyyy→y. Let’s prove that they give a unique result with the diamond lemma. Suppose we have some string and two possible rules that apply. If we apply the rules to nonoverlapping substrings, then after applying one rule we can just apply the other, so both paths reach the same place. Now we just check overlapping substrings. We have a few possible overlaps. There’s (xx)y=x(xy) and (xy)yyy=x(yyyy), but also (xx)x=x(xx) and some overlaps with five, six, or seven ys. We resolve the first two overlaps with the following diagrams.
For the overlaps consisting only of xs or ys, the result after any two applications of a rule is already the same. We’ve proved the diamond property for our simplification rules! Now we just need to prove termination. We can only apply rule two (xy→yyx) to the last x finitely many times before it crosses all ys to the right of it and is at the back of our string. Then this last x can produce only finitely many extra ys, so the second-to-last x can only move right finitely many times, and so on. Thus rule 2 can only be applied finitely many times overall. The other rules decrease the number of letters in our string, so they can also only be applied finitely many times. We’ve proved that in the monoid with two variables and relations x2=1 and xy=y2x, these three simplification rules are all we need to determine equality! This lets us easily see that for example y2≠y.
Exercise for the reader: What if we try to always decrease the number of letters, so that our second simplification rule is instead yyx→xy? What is our final list of simplification rules?
Rings
You can do the same thing with a ring instead of a monoid. It’s a bit more technical, but it turns out that if your simplification rules have a monomial on the left side (e.g. xyx→yyx+1), you can check for overlaps in the obvious way. You’ll probably want to use a monomial ordering to prove termination.
Exercise: take 𝔽2 and add some variables x and y such that x2=1 and xy=y2x+1.
Formal statement and proof
Lemma
Let G be a directed graph with no infinite chain (i.e. if you start at any vertex and travel forwards along the directed edges, you must eventually reach a vertex with no outgoing edges). Suppose that for any vertex v of G, if a and b are children of v (i.e. there is an edge v→a and v→b), there exists some vertex t of G such that there is a path a→…→t in G from a to t and a path b→…→t from b to t. Then for any vertex v, there exists some vertex s with no outgoing edges such that any vertex reachable from v has a path to s.
Proof
Fix some vertex v of G, and fix some s with no outgoing edges that is reachable from v. Let P be the set of vertices a in G such that s is reachable from a and all of its descendants. It suffices to show that v is in P. Note that s is in P, since s has no descendants. Note also that for any element of P, all its descendants are in P, and if all children of a nonterminal vertex are in P, then the vertex is itself in P.
Define a set Q to be the set of all vertices of G that have at least one child in P and at least one child that is not in P.
Note that if a vertex a has some descendant p in P, then either a is in P, a is in Q, or a has a descendant in Q: if a is not in P, then take the last vertex b along the path from a to p that is not in P. Then b has a child in P (the next vertex on the path) and a child that is not in P (or else b would itself be in P), so b is in Q, and b is either a or one of its descendants.
I claim that any element of Q has a descendant that is also in Q. Let a be an element of Q. Then it has children b and c, where b is in P and c is not in P. Applying the diamond property, there exists a vertex t that is reachable from both b and c. Then t must be in P because it is reachable from b. Then c is not in P but has a descendant in P, so either c is in Q or one of its descendants is in Q. Either way, a has a descendant in Q.
Now if Q were nonempty, it would have some element, which would have a descendant in Q, which would itself have a descendant in Q, etc., so we would have an infinite chain, which is impossible. Thus Q is empty, so if a vertex has a child in P, all its children are in P and it is thus itself in P, so any ancestor of a vertex in P is also in P. We know that s is in P and v is an ancestor of s, so v is in P and the lemma is proved.