a locally confluent and terminatting rewrite system is complete

Question

I want to prove that every locally confluent rewrite system is confluent. Since I know very little about rewrite systems and logic, I tried looking at it as a digraph with no external infinite paths and with the locally confluent property but I could only prove it in very specific cases such as when every path in the digraph has length two. Any hints to proving this would be very helpful.

Answer 1

The basic technique is essentially filling diamonds. Local confluence says that whenever we have $b\gets a\to c$ we obtain a $d$ such that $b\to^*d\gets^*c$. This is often drawn as a diamond with $a$ at the top and $d$ at the bottom. For confluence, we want to extend this to assuming $b\gets^* a\to^* c$, meaning we have multiple steps to get to $b$ and $c$. In this case it can be pictured as a grid of diamonds, where the assumption fills in all the inner diamonds until we get down to the $d$ we want at the bottom.

That's only a sketch, but it works... provided that we know that $b\gets a\to c$ implies there exists $b\to d\gets c$, with no multiple steps at the bottom of the diamond. With multiple steps, as in our assumption of local confluence, each diamond we complete produces even more diamonds to fill, which themselves may make more work than they solve. This is the purpose of the second assumption, termination, which ensures that the total amount of work to do is finite.

---

How can we write this formally? Every term has a tree (well, dag) of rewrites that stem from it. Since there are no infinite paths in this tree, we can assign an ordinal $h(a)$ to each term $a$ such that $a\to b$ implies $h(a)>h(b)$. An easy way to construct this measure is to set $$h(a)=\sup_{b \mathrm{\ s.t.\ }a\to b}h(b)+1.$$

Theorem: (Assuming $\to$ is locally confluent and terminating:) If $b\gets^* a\to^* c$, then there exists $d$ such that $b\to^*d\gets^*c$.

Proof: By induction on $h(a)$. If $a=b$ then take $d=c$. If $a=c$ then take $d=b$. Otherwise we have $b\gets^* b'\gets a\to c'\to^* c$ (see figure), and from local confluence we have $b'\to^*d'\gets^*c'$. But now, since $a\to b'$ and $a\to c'$, we have $h(b')<h(a)$ and $h(c')<h(a)$, as well as $b\gets^*b'\to^*d'\gets^*c'\to^*c$, so from the induction hypothesis applied to $b'$ and $c'$, we have $e,f$ such that $b\to^*e\gets^*d'\to^*f\gets^*c$. Finally, since $a\to b'\to^*d'$ we have $h(a)>h(b)\ge h(d')$, so we can apply the inductive hypothesis once more on $e\gets^*d'\to^*f$ to get $d$ such that $e\to^*d\gets^*f$, and so $b\to^*e\to^*d\gets^*f\gets^* c$ and $d$ is as desired.

$$\begin{array}{ccccccccc} &&&& a\\ &&&\!\!\!\!\swarrow\!\!\!\! && \!\!\!\!\searrow\!\!\!\!\\ && b' &&&& c'\\ &\!\!\!\!\swarrow^*\!\!\!\! && \!\!\!\!\searrow^*\!\!\!\! && \!\!\!\!\swarrow^*\!\!\!\! && \!\!\!\!\searrow^*\!\!\!\!\\ b &&&& d' &&&& c\\ & \!\!\!\!\searrow^*\!\!\!\! && \!\!\!\!\swarrow^*\!\!\!\! && \!\!\!\!\searrow^*\!\!\!\! &&\!\!\!\!\swarrow^*\!\!\!\!\\ && e &&&& f\\ &&&\!\!\!\!\searrow^*\!\!\!\! && \!\!\!\!\swarrow^*\!\!\!\!\\ &&&& d \end{array}$$

---

An alternative to the proof using the ordinal function $h(a)$ is to proceed by contradiction, constructing an infinite path starting at $a$. Suppose that $a$ fails the theorem. If $b',c',d'$ all satisfy the inductive hypothesis then we are golden by the above proof. Otherwise one of these is a counterexample (say $d'$) and we have a path $a\to^+d'$ (where $\to^+$ means that the path consists of one or more reductions). We can state this as a theorem: for any counterexample point $a$, there exists another counterexample point $a'$ which is reachable from $a$ by one or more reductions. By iterating this we obtain an infinite path $a\to^+a'\to^+a''\to\dots$, contradicting termination.