Give decidable criteria for left-linear rewriting systems to be Church-Rosser.

The source page states the original problem together with its recorded qualifications and progress updates as follows.

By a lemma of G'erard Huet [L'evy, 1991], left-linear term-rewriting systems are confluent if, for every critical pair $t \approx s$ (where $t = u[r\sigma] \leftarrow u[l\sigma] = g\tau \rightarrow d\tau = s$, for some rules $l \rightarrow r$ and $g \rightarrow d$), we have $t \rightarrow^\| s$ ($t$ reduces in one parallel step to $s$). (The condition $t \rightarrow^\| s$ can be relaxed to $t \rightarrow^\| r \leftarrow^\| s$ for some $r$ when the critical pair is generated from two rules overlapping at the roots; see [L'evy, 1991].) What if $s \rightarrow^\| t$ for every critical pair $t \approx s$? What if for every $t \approx s$ we have $s \rightarrow^= t$? (Here $\rightarrow^=$ is the reflexive closure of $\rightarrow$.) What if for every critical pair $t \approx s$, either $s \rightarrow^= t$ or $t \rightarrow^= s$? In the last case, especially, a confluence proof would be interesting; one would then have confluence after critical-pair completion without regard for termination. If these conditions are insufficient, the counterexamples will have to be (besides left-linear) non-right-linear, non-terminating, and non-orthogonal (have critical pairs). See [L'evy, 1991].

Recorded progress.

Significant progress is reported in [L'evy, 1991].

A new criterion based on so-called simultaneous critical pairs has been presented in~[L'evy, 1991].

The history of the problem and the attempts to solve it are told in [L'evy, 1991].