I have been meaning to post about this wonderful paper, which you can read here, for quite some time now.  It has sealed a spot as one of my two favorite papers of 2010.  In it, Nao Hirokawa and the incredibly productive Aart Middeldrop (I chaired a session at IJCAR 2010 consisting solely of papers co-authored by Aart — wow) give a new criterion for confluence, based on relative termination.  As the abstract to the paper says:

In this paper we use the decreasing diagrams technique to show that a left-linear term rewrite system R is confluent if all its critical pairs are joinable and the critical pair steps are relatively terminating with respect to R.

I mentioned relative termination in a post earlier this year (which was supposed to provide background for talking a little about this paper, but I didn’t manage to post about it until now).  A term-rewriting system R is relatively terminating with respect to another S iff the relation $\rightarrow_{R/S}$ defined to be $\rightarrow_S^* \cdot \rightarrow_R \cdot \rightarrow_S^*$ is terminating.  This of course implies that R is terminating, since $\rightarrow_R \subseteq \rightarrow_{R/S}$: if we forbid an infinite sequence of R-steps where in between every two R-steps we are allowed also to have a finite number of S-steps, then we are certainly forbidding an infinite sequence of R-steps with no S-steps in between any two R-steps.  But we can easily describe systems R which are terminating but not terminating relative to some other systems S.

The criterion (for left-linear rewrite systems — that is, rewrite systems where no variable is allowed to appear twice on the left hand side of a rule, as in $\textit{eq}(x,x) \rightarrow \textit{true}$) that all critical pairs are joinable and the rewrite system consisting of critical pair steps is relatively terminating with respect to R generalizes the two best known confluence criteria: the Knuth-Bendix criterion, which requires joinability of critical pairs (I’ll explain those in a moment) for terminating rewrite systems; and the orthogonality criterion, which requires the absence of overlaps in left-hand sides of rules, but does not require termination.  A critical pair of two (possibly the same) rewrite rules is the pair of terms you get from overlapping the two rules in a non-trivial way.  For example, consider the single rule $f(f(x,y),z) \to f(x,f(y,z))$, expressing associativity of an operation $f$.  This rule can be overlapped non-trivially with itself by unifying the whole term with the $f(x,y)$ subterm.  In this case, we get two critical pair steps: $f(f(f(x',x''),y),z) \rightarrow f(f(x',x''),f(y,z))$ and $f(f(f(x',x''),y),z) \rightarrow f(f(x',f(x'',y)),z)$.  The critical pair itself consists of the two right hand sides of these rules.  If the critical pair steps are terminating relative to the rewrite system R (and if the set of rules is left-linear), then Hirokawa and Middeldorp have shown that we get confluence.

The reason I am so impressed with this paper is that it generalizes these two well-known confluence criteria.  It generalizes the Knuth-Bendix criterion because it does not require termination (but still requires joinability of critical pairs).  It generalizes the orthogonality criterion because there, since there are no critical pairs, the set of critical pair steps is trivially terminating with respect to the rewrite system (since we have no critical pair steps to take, we cannot possibly diverge taking them).  Also, the proof uses decreasing diagrams, an advanced characterization of confluence in terms of diagrams due to Vincent van Oostrom.  So the technical machinery required is pretty sophisticated.

Below is a picture of Nao which I took right after his presentation, with a diagram he drew illustrating the essential idea of the theorem: