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

Problem #47 (Solved !)

Originator: Jan Willem Klop
Date: December 1991

Summary: Prove a Parallel Moves Lemma for reductions of infinite length.

For reductions of transfinite length, a version of the Parallel Moves Lemma can be proved if one considers only “strongly converging” infinite reductions in the sense of [KKSd91]. However, if one wants to consider converging reductions, as in [DKP91], then it is not difficult to construct a counterexample, not to the infinite Parallel Moves Lemma itself, but to the method of proof (cf. [KKSd90]). An infinite Parallel Moves Lemma might involve a different notion of “descendant”.

Remark

[Sim04] shows that it is not possible to obtain a Parallel Moves Lemma for (Cauchy-)convergent infinite reductions which relies on a notion of residual maintaining some of the basic properties of residuals known from the finite case. His counterexamples, however, are somewhat particular in that the right-hand sides of the rewrite rule are not normalized. The question remains whether it is possible to salvage a Parallel Moves Lemma for (Cauchy-)convergent reductions for restricted classes of rewrite systems.

References

[DKP91]
Nachum Dershowitz, Stéphane Kaplan, and David A. Plaisted. Rewrite, rewrite, rewrite, rewrite, rewrite,…. Theoretical Computer Science, 83(1):71–96, 1991.
[KKSd90]
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.
[KKSd91]
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.
[Sim04]
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]