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