[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #26

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:

• if in rewrite step t →_R t′ redex r in t and redex r′ in t′ are such that r′ is a descendant (or “residual”) of r, then #r ≥ #r′;
• if in rewrite step t → 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′.

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?

Comment sent by Vincent van Oostrom

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].

References

[Klo80]

Jan Willem Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1980.

[Mel96]

Paul-André Melliès. Description Abstraite des Systèmes de Réécriture. Thèse de doctorat, Université Paris VII, 20 Décembre 1996.

[Oos97]

Vincent van Oostrom. Finite family developments. In Hubert Comon, editor, 8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, pages 308–322, Barcelona, Spain, June 1997. Springer-Verlag.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]