[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Jan Willem Klop
Date: April 1991
Summary: 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?
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:
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 [Klo80] 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?
Date: Thu Mar 4 11:28:20 MET 1999
Contrary to what was claimed in [Klo80] (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 [Mel96], pp. 158-160.
The main application of the lemma, termination of rewrite systems having ‘bounded production-depth’, was recovered there ([Mel96], Theorem 6.5) in an axiomatic setting. For the case of higher-order rewriting this was shown in [Oos97].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |