\documentclass{rtaloop}
\rtalabel{levy}


\begin{document}
\begin{problem}{Jean-Jacques L\'evy}{}{April 1991}

\begin{abstract}
  Give decidable criteria for left-linear rewriting systems to be
  Church-Rosser.
\end{abstract}

By a lemma of G\'erard Huet \cite{H80:jacm}, 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
\cite{T88:pfgc}.) 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 \cite{K92:ox}.


\begin{remark}
  Significant progress is reported in \cite{OO97}.
  
  A new criterion based on so-called {\em simultaneous critical pairs}
  has been presented in~\cite{Okui:rta98}.

  The history of the problem and the attempts to solve it are told in
  \cite{Dershowitz05OpenClosed}.
\end{remark}


\end{problem}
\end{document}