\documentclass{rtaloop}
\rtalabel{many-sorted}

\begin{document}
\begin{solvedproblem}{Hans Zantema}{}{June 1993}

\begin{abstract}
Does termination of a many-sorted rewrite system reduce to the one-sorted case
in case all variables are of the same sort?
\end{abstract}

Let $R$ be a many-sorted term-rewriting system and $R'$ the one-sorted system
consisting of the same rules, but in which all operation symbols are
considered to be of the same sort. Any rewrite in $R$ is also a rewrite in
$R'$. The converse does not hold, since terms and rewrite steps in $R'$ are
allowed that are not well-typed in $R$. In \cite{Z94} it was shown that
termination of $R$ is in general not equivalent to termination of $R'$, but it
is if $R$ does not contain both collapsing and duplicating rules. Are
termination of $R$ and of $R'$ equivalent in the case where all variables
occurring in $R$ are of the same sort? If this statement holds, it would
follow that simulating operation symbols of arity $n$ greater than 2 by $n-1$
binary symbols in a straightforward way does not affect termination behavior.

\begin{remark}
This has been solved positively by Takahito Aoto \cite{Takahito2001jflp}. 
\end{remark}

\end{solvedproblem}
\end{document}