| [Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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 t → s 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.
| [Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |