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?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

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}

1. 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'$;

2. 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 [Klop, 1991] 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?

Recorded update.

Submitted by Vincent van Oostrom on Thu Mar 4 11:28:20 MET 1999.

Contrary to what was claimed in [Klop, 1991] (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 [Klop, 1991], pp. 158-160.

The main application of the lemma, termination of rewrite systems having `bounded production-depth', was recovered there ([Klop, 1991], Theorem 6.5) in an axiomatic setting. For the case of higher-order rewriting this was shown in [Klop, 1991].