\documentclass{rtaloop}
\rtalabel{modularity}

\begin{document}
\begin{problem}{M. Kurihara, M. Krishna Rao}{}{June 1993}

\begin{abstract}
What are sufficient condition for the modularity of confluence?
\end{abstract}

One of the earliest results established on modularity of combinations of
term-rewriting systems is the confluence of the union of two confluent systems
which share no symbols \cite{T87:jacm}; if symbols are shared modularity is
not preserved by union \cite{KO92:tcs}. Some sufficient conditions for
modularity of confluence of constructor-sharing systems that are terminating
have been found \cite{KO92:tcs}\cite{MT91:rta}. Are there interesting
sufficient conditions that are independent of termination?


\begin{remark}
Left-linearity is a sufficient condition, as shown long ago in
\cite{RV80:jacm}. In \cite{Ohlebusch:caap94}, it is established that
confluence is modular in the presence of the weak normalization property.
(This result has been extended in \cite{Kri95,Kri98} for hierarchical
combinations.) In \cite{D97:rta}, some results are given when only one of the
systems is terminating.

There are other sufficient conditions for modularity of confluence that do not
require termination of the combined system even when function symbols are
shared. One set of conditions, viz., ``persistence'', ``relative
termination'', and $lr$-disjointness, is given in \cite{Verma95,Verma96}. An
abstract confluence theorem without termination is given in \cite{Geser:PhD}.
\end{remark}

\end{problem}
\end{document}