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

Problem #13

Originator: Jean-Jacques Lévy
Date: April 1991

Summary: Give decidable criteria for left-linear rewriting systems to be Church-Rosser.

By a lemma of Gérard Huet [Hue80], left-linear term-rewriting systems are confluent if, for every critical pair t ≈ s (where t = u[rσ] ← u[lσ] = gτ → dτ = s, for some rules l → r and g → d), we have t →||s (t reduces in one parallel step to s). (The condition t →||s can be relaxed to t →||r ←||s for some r when the critical pair is generated from two rules overlapping at the roots; see [Toy88].) What if s →||t for every critical pair t ≈ s? What if for every t ≈ s we have s →= t? (Here →= is the reflexive closure of →.) What if for every critical pair t ≈ s, either s →= t or t →= s? In the last case, especially, a confluence proof would be interesting; one would then have confluence after critical-pair completion without regard for termination. If these conditions are insufficient, the counterexamples will have to be (besides left-linear) non-right-linear, non-terminating, and non-orthogonal (have critical pairs). See [Klo92].

Remark

Significant progress is reported in [OO97].

A new criterion based on so-called simultaneous critical pairs has been presented in [Oku98].

The history of the problem and the attempts to solve it are told in [Der05].

References

[Der05]
Nachum Dershowitz. Open. Closed. Open. In Jürgen Giesl, editor, 16th International Conference on Rewriting Techniques, volume 3467 of Lecture Notes in Computer Science, Nara, Japan, April 2005. Springer-Verlag.
[Hue80]
Gérard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. of the Association for Computing Machinery, 27(4):797–821, October 1980.
[Klo92]
Jan Willem Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–117. Oxford University Press, Oxford, 1992.
[Oku98]
Satoshi Okui. Simultaneous critical pairs and Church-Rosser property. In Tobias Nipkow, editor, 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 2–16, Tsukuba, Japan, April 1998. Springer-Verlag.
[OO97]
Michio Oyamaguchi and Yoshikatsu Ohta. A new parallel closed condition for Church-Rosser of left-linear term rewriting systems. In Hubert Comon, editor, 8th International Conference on Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, pages 187–201, Barcelona, Spain, June 1997. Springer-Verlag.
[Toy88]
Yoshihito Toyama. Commutativity of term rewriting systems. In K. Fuchi and L. Kott, editors, Programming of Future Generation Computers II, pages 393–407. North-Holland, 1988.

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