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


\begin{document}
\begin{problem}{Yoshihito Toyama}{}{April 1991}

\begin{abstract}
Under what conditions does confluence of a normal semi-equational conditional
term rewriting system imply confluence of the associated oriented system?
\end{abstract}

For a \emph{normal} conditional term-rewriting system $R = \{ s
\rightarrow^! t \Rightarrow l \rightarrow r \}$, where $t$ must be a
ground normal from of $s$, we can consider the corresponding
semi-equational conditional rewrite system $R_{se} = \{ s
\leftrightarrow^* t \Rightarrow l \rightarrow r \}$. Under what
conditions does confluence of $R_{se}$ imply confluence of $R$?  In
general, this is not the case, as can be seen from the following
non-confluent system $R$ (due to Aart Middeldorp):

\begin{eqnarray*}
a \rightarrow b\\
a \rightarrow c\\
b \rightarrow^! c \Rightarrow    b \rightarrow c
\end{eqnarray*}


\begin{remark}
Solutions have been provided by \cite{yamada00tcs}. They show that
confluence of $R$ follows from confluence of $R_{se}$ if any of the two
following conditions is satisfied:
\begin{itemize}
\item $R_{se}$ is semi-decreasing
\item $R_{se}$ is level-confluent
\end{itemize}
See \cite{yamada00tcs} for definitions of these properties.
\end{remark}

\end{problem}
\end{document}