[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #62 (Solved !)

Originator: Vincent van Oostrom
Date: June 1993

Summary: Is the union of two left-linear, confluent combinatory reduction systems over the same alphabet, where the rules of the first system do not overlap the rules of the second, confluent?

Let R and S be two left-linear, confluent combinatory reduction systems with the same alphabet. Suppose the rules of R do not overlap the rules of S. Is R ∪ S confluent? This is true for the restricted case when R is a term-rewriting system (an easy generalization of a result by F. Müller [Mül92]), or if neither system has critical pairs. (The restriction to the same alphabet is essential, since confluence is in general not preserved under the addition of function symbols, not even for left-linear systems.)

Remark

The answer is yes (Thm. 3.1 of [vOvR94]).

References

[Mül92]

Fritz Müller. Confluence of the lambda calculus with left-linear algebraic rewriting. Information Processing Letters, 41:293–299, April 1992.

[vOvR94]

Vincent van Oostrom and Femke van Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In A. Nerode and Y. V. Matiyasevich, editors, Third International Symposium on the Logical Foundations of Computer Science, volume 813 of Lecture Notes in Computer Science, pages 379–392, St. Petersburg, Russia, July 1994. Springer-Verlag.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]