\documentclass{rtaloop}
\rtalabel{decreasing-redex}

\begin{document}
\begin{problem}{Jan Willem Klop}{}{April 1991}


\begin{abstract}
Is it true for non-orthogonal systems that decreasing redexes implies
termination? If not, can some decent subclasses be delineated for which the
implication does hold?
\end{abstract}


Let $R$ be a term-rewriting or combinatory reduction system. Let ``decreasing
redexes'' (DR) be the property that there is a map $\#$ from the set of
redexes of $R$, to some well-founded linear order (or ordinal), satisfying:
\begin{itemize}
\item if in rewrite step $t \rightarrow_R t'$ redex $r$ in $t$ and
  redex $r'$ in $t'$ are such that $r'$ is a descendant (or
  ``residual'') of $r$, then $\#r \geq \#r'$;
\item if in rewrite step $t \rightarrow t'$ the redex $r$ in $t$ is
  reduced and $r'$ in $t'$ is ``created'' ($t'$ is not the descendant
  of any redex in $t$), then $\#r > \#r'$.
\end{itemize}

Calling $\#r$ the ``degree'' of redex $r$, created redexes have a
degree strictly less than the degree of the creator redex, while the
degree of descendant redexes is not increased. The typical example is
reduction in simply typed lambda calculus.  In \cite{K80:mct} it is
proved that for orthogonal term- rewriting systems and combinatory
reduction systems, decreasing redexes implies termination (strong
normalization).  Does this implication also hold for non-orthogonal
systems?  If not, can some decent subclasses be delineated for which
the implication does hold?

\begin{submitted}{Vincent van Oostrom}{Thu Mar  4 11:28:20 MET 1999}

Contrary to what was claimed in \cite{K80:mct} (and in the statement of
problem 26), decreasingness does not imply termination for orthogonal
combinatory reduction systems. A counterexample can be found in Section 6.2.2
of the PhD thesis \cite{Mellies:these}, pp. 158-160.

The main application of the lemma, termination of rewrite systems having
`bounded production-depth', was recovered there (\cite{Mellies:these}, Theorem
6.5) in an axiomatic setting. For the case of higher-order rewriting this was
shown in \cite{Oostrom97rta}.

\end{submitted}



\end{problem}
\end{document}