Right Angled Coxeter Group Proof.md

This gives a proof of correctness of the algorithm at node_string.rs. Unless otherwise specified, lowercase letters are used for variables for single symbols and group generators, and uppercase letters are used for variables for strings and group elements. 1 is the empty string or the identity element of a group. X$Y means every symbol of A commutes with every symbol of B (as group generators).

Let G be a right-angled coxeter group over the set of generators S. This just means that G is a group presented by aa = 1 for each a in S and any set of equations of the form ab = ba (or equivalently abab = 1) for a ≠ b. In addition, there is a linear order < over S.

The algorithm rewrites strings of the form Xa into a canonical form, assuming X is already in said canonical form. It maintains index variables i and j initialized to the length of X. Start a loop. If the ith element of X is a, return X with ith element removed and end the algorithm. If the ith element does not commute with a, break the loop. If a < the ith element of X, set j := i. Decrement i. End loop. Return X with a inserted before position j.

The theorem to be proved is that the above algorithm rewrites string X and Y into the same normal form if they are equivalent according to the group presentation.

First, we shall work with an abstract rewriting system related to the above algorithm. It rules are of the form:

1. aa -> 1 for each generator a in G
2. bXa -> abX if a < b and a$bX

Theorem 1: the equations implied by the rewriting system are equivalent to the equations of G.

First we shall prove that the equations of G imply the rewriting system equations. Rule (1) is implied by aa = 1 and rule (2) is implied by the fact that a commutes with xB for each generator in xB.

Next, we show that the rewriting system equations imply the group equations:

• Associativity and identity: implied by the fact the equations are coming from a string rewriting system
• aa = 1 for each a in S: implied by rule (1)
• Inverses: each generator is its own inverse, so implied by the previous point
• ab = ba: If a < b, then ba -> ab is an instance of rule (2). If b < a, then ab -> ba is an instance of rule (2). If a = b, the equation is trivial.

∎

Lemma 2.1: If a$X, then (aX, Xa) is a confluent pair, meaning there is a W such that aX and Xa can be written into W using some sequence of steps.

In the string Xa, use rule (2) to move the a in Xa as far left as possible to get Xa -> YaZ, where X = YZ. This implies y <= a for each in y in Y, since otherwise it could be moved farther left. This means that aYZ -> YaZ by moving each symbol of Y to the left of a, one symbol at a time (using rule (2) if y < a or trivially if y = a). The pair is confluent.

Theorem 2: The rewriting system is locally confluent, which means that for any string Z, if it can be rewritten into X in a single step or into Y in a single step, (X, Y) is a confluent pair.

We will use the critical pair lemma. We will assume a < b and c < d < e unless otherwise specified. Parentheses are added for clarity.

• Critical pairs generated by rule 1 with itself
  • a(a)a gives the critical pair (1a, a1) for both sides. 1a and a1 are both equal to a, so the pair is confluent.
• Critical pairs generated by rule 1 with rule 2
  • b(b)Xa gives the pair (Xa, b(abX)) if a$bX. First, rewrite babX -> abbX -> aX. Since a$X, the pair (Xa, aX) is confluent by lemma 2.1.
  • (bb)Xa gives the pair (Xa, abbX) if a$bbX. First rewrite abbX -> aX. Since a$X, the pair (Xa, aX) is confluent by lemma 2.1.
  • bX(cc)Ya gives the pair (bXYa, abXccY) if a$bXccY. Then bXYa -> abXY and abXccY -> abXY. The pair is confluent.
  • bX(aa) gives the pair (abXa, bX) if a$bXa. Then abXa -> aabX -> bX. The pair is confluent.
  • bX(a)a gives the pair ((abX)a, bX) if a$bX. The previous point shows this pair is confluent.
• Critical pairs generated by rule 2 with itself
  • eX(d)Yc gives the pair ((deX)Yc, eX(cdY)) if d$eX and c$dY. Note that by the second condition c$d. Rewrite eXcdY -> deXcY. Since c$Y, the pair (Yc, cY) is confluent by lemma 2.1, making (deXYc, deXcY) confluent.
  • dX(bYc)Za gives the pair ((cdXbY)Za, dX(abYcZ)) if a$(bYcZ) and c$(dXbY). Note that the first condition implies a$c. Then dXabYcZ -> cdXabYZ by applying rule (2) to c and cdXbYZa -> cdXabYZ applying rule (2) to a. The pair is confluent.
  • (eXd)Yc gives the pair ((deX)Yc, ceXdY) if d$eX and c$eXdY. Then deXYc -> cdeXY and ceXdY -> cdeXY. The pair is confluent.
  • bX(dYc)Za gives the pair (bX(cdY)Za, abXdYcZ) if a$bXdYcZ and c$dZ. Then abXdYcZ -> abXcdYZ by applying rule(2) to d and bXcdYZa -> abXcdYZ by applying rule (2) to a. The pair is confluent.
  • eX(dYc) gives the pair (eX(cdY), ceXdY)) if c$eXdY. Then eXcdY -> ceXdY. The pair is confluent.

Therefore, the hypotheses of the critical pair lemma are satisfied, and the rewriting system is locally confluent. ∎

Theorem 3: the rewriting system is confluent (a.k.a. globally confluent).

Note that the rewriting system always decreases terms with respect to shortlex with the order on symbols being <. This is because when rule (1) rewrites YaaZ -> YZ, the string is shortened, and when rule(2) rewrites YbXaZ -> YabXZ, the string is the same length but it is lexicographically smaller. Since any sequence in decreasing shortlex order is finite (length at most (|S|+1)^n if n is the length of the first string) and the rewriting system is locally confluent by theorem 2, the rewriting system is globally confluent by Newman's lemma. ∎

Corollary 3.1: the rewriting system satisfies the normal form property

Theorem 3 implies confluence and confluence implies the normal form property. ∎

Theorem 4: Two strings represent the same element in G iff they have the same normal form under the rewriting system.

Theorem 1 implies the (<-) direction. For the (->) direction, note that representing the same element means that one string can be shown equivalent to the other using the group presentation equations, which by theorem 1 is equivalent to them being shown equivalent using the rewriting system equations, which by corollary 3.1 is equivalent to them having the same normal form. ∎

Theorem 5: The algorithm described at the top calculates the normal form of the rewriting system.

We are given a string Xa where X is already in canonical form. By induction, we will assume that X is a normal form of the abstract rewriting system. The algorithm is sound with respect to the equations because:

• It can only be inserted before position j if it commutes with everything at positions including and after j. This is valid because the equations imply the commutation equations by theorem 1.
• If the algorithm terminates by deleting the element at index is, this is valid through the combination of commutation (as in the previous point) and then rewriting aa -> 1.

The algorithm returns a normal form because:

• If the algorithm terminates by inserting a, this is a normal form because:
  • No rewrite rule could move a further left by rule (2)
  • It won't be deleted by rule (1) since otherwise it would return a different way
  • Rule (2) won't move anything to the right of i. If it did move something at, say, j > i to the left, it would need to move it directly left of i, since moving it to any other position contradicts the fact that X is a normal form. By the definition of rule (2), this means the element at j commutes with everything in the interval [i, j), and the symbol at j is < a. However, a < the symbol at i + 1, which means the symbol at j < the symbol at i + 1. This means rule (2) could have moved the symbol at j to the left of the symbol at i + 1, contradicting the fact that X is a normal form. Contradiction. So the assumption that rule (2) could move any symbol that was at a position right of i is false.
• If the algorithm terminates by deleting the a at index i:
  • rule (1) can't be applied at the boundary because that would imply a pattern cac at the boundary (for some generator c), and this can be rewritten to acc or cca by rule (2) since a$c, which contradicts X being in normal form.
  • rule (2) can't be applied because if a was preventing a use of rule (2), that means it didn't commute with anything to the right of i, which means there are no positions to the right of i (since otherwise this would contradict that everything to the right of i commutes with a), and deleting a symbol at the end of the string can't enable a new use of rule (2).

∎

Theorem 6: Two strings represent the same element in G iff the algorithm calculates the same result for them.

This is just the combination of theorem 4 and theorem 5. ∎