\documentclass{rtaloop}
\rtalabel{infinite-confluence}


\begin{document}
\begin{solvedproblem}%
  {Richard Kennaway, Jan Willem Klop, Ronan Sleep, Fer-Jan de Vries}%
  {\cite{KKSV91:rta}}%
  {April 1991}

\begin{abstract}
  Does ``almost-confluence'' hold for convergent infinite reduction sequences?
\end{abstract}

If one wants to consider reductions of transfinite length in the theory of
orthogonal term-rewriting systems, one has to be careful. In
\cite{KKSV90:cwi}\cite{KKSV91:rta} it is shown that the confluence property
``almost'' holds for infinite rewriting with orthogonal term-rewriting
systems. The only situation in which ``infinitary confluence'' may fail is
when collapsing rules are present. (A rule $t \rightarrow s$ is ``collapsing''
if $s$ is a variable.) Without collapsing rules, or even when only one
collapsing rule of the form $f(x) \rightarrow x$ is present, infinitary
confluence does hold.

Now the notion of infinite reduction in \cite{KKSV91:rta} is based upon
``strong convergence'' of infinite sequences of terms in order to define
(possibly infinite) limit terms. In related work, Dershowitz, et al.
\cite{DKP91:tcs} use a more ``liberal'' notion of convergent sequences (which
is referred to in \cite{KKSV91:rta} as ``Cauchy convergence''). What is
unknown (among other questions in this new area) is if this
``almost-confluent'' result is also valid for the more liberal convergent
infinite reduction sequences?

\begin{remark}
  This has been answered to the negative by \cite{simonsen04ipl}. However, the
  counter-example given there is quite peculiar: The rewrite system is not
  right-linear, the right-hand sides of the rules are not in normal form, and
  there is no bound on the depths of the left-hand sides of the rules (the
  rewrite system has an infinite number of rules). Thus, the question remains
  under which reasonable conditions (Cauchy-)convergent and orthogonal rewrite
  systems are almost-confluent.
\end{remark}

\end{solvedproblem}
\end{document}