\documentclass{rtaloop}
\rtalabel{occur-check}
\begin{document}
\begin{problem}{Mizuhito Ogawa}{}{April 1995}
\begin{abstract}
Does a system that is nonoverlapping under unification with infinite
terms have unique normal forms?
\end{abstract}
Does a system that is nonoverlapping under unification with infinite
terms (unification without ``occur-check'' \cite{Martelli:84}) have
unique normal forms? This conjecture was originally proposed in
\cite{OgawaOno:89} with an incomplete proof, as an extension of the
result on strongly nonoverlapping systems
\cite{K80:mct}\cite{C81:stoc}. Related results appear in
\cite{OO93:ieice}\cite{Toyama94}\cite{ManoOgawa:94}, but the original
conjecture is still open. This is related to Problem 58. This
problem is also related with modularity of confluence of systems
sharing constructors, see \cite{ohlebusch94}.
\begin{remark}
The answer is yes if the system is also nonduplicating \cite{Rak96}.
A direct technique is given in \cite{Rak96}. The nonduplicating
condition can be relaxed under a certain technical condition
\cite{Rak96}. Some extensions to handle root overlaps are given in
\cite{Rak97} and a restricted version of the result in
\cite{C81:stoc} is also proved using the direct technique in
\cite{Rak97}.
\end{remark}
\end{problem}
\end{document}