[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #18 (Solved !)

Originator: Richard Kennaway, Jan Willem Klop, Ronan Sleep, Fer-Jan de Vries [KKSd91]
Date: April 1991

Summary: Does “almost-confluence” hold for convergent infinite reduction sequences?

If one wants to consider reductions of transfinite length in the theory of orthogonal term-rewriting systems, one has to be careful. In [KKSd90][KKSd91] it is shown that the confluence property “almost” holds for infinite rewriting with orthogonal term-rewriting systems. The only situation in which “infinitary confluence” may fail is when collapsing rules are present. (A rule ts is “collapsing” if s is a variable.) Without collapsing rules, or even when only one collapsing rule of the form f(x) → x is present, infinitary confluence does hold.

Now the notion of infinite reduction in [KKSd91] is based upon “strong convergence” of infinite sequences of terms in order to define (possibly infinite) limit terms. In related work, Dershowitz, et al. [DKP91] use a more “liberal” notion of convergent sequences (which is referred to in [KKSd91] as “Cauchy convergence”). What is unknown (among other questions in this new area) is if this “almost-confluent” result is also valid for the more liberal convergent infinite reduction sequences?


This has been answered to the negative by [Sim04]. However, the counter-example given there is quite peculiar: The rewrite system is not right-linear, the right-hand sides of the rules are not in normal form, and there is no bound on the depths of the left-hand sides of the rules (the rewrite system has an infinite number of rules). Thus, the question remains under which reasonable conditions (Cauchy-)convergent and orthogonal rewrite systems are almost-confluent.


Nachum Dershowitz, Stéphane Kaplan, and David A. Plaisted. Rewrite, rewrite, rewrite, rewrite, rewrite,…. Theoretical Computer Science, 83(1):71–96, 1991.
J. R. Kennaway, Jan Willem Klop, M. R. Sleep, and F. J. de Vries. Transfinite reductions in orthogonal term rewriting systems. Technical Report CS-R9041, CWI, Amsterdam, 1990.
J. R. Kennaway, Jan Willem Klop, M. R. Sleep, and F. J. de Vries. Transfinite reductions in orthogonal term rewriting systems (Extended abstract). In Ronald. V. Book, editor, 4th International Conference on Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer Science, pages 1–12, Como, Italy, April 1991. Springer-Verlag.
Jakob Grue Simonsen. On confluence and residuals in Cauchy convergent transfinite rewriting. Information Processing Letters, 91(3):141–146, August 2004.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]