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


Problem #58

Originator: Michio Oyamaguchi
Date: June 1993

Summary: Is any “strongly” non-overlapping right-linear term-rewriting system confluent?

Is any “strongly” non-overlapping right-linear term-rewriting system confluent? (“Strong” in the sense that left-hand sides are non-overlapping even when the occurrences of variables have been renamed apart [Che81].) On the one hand, strongly non-overlapping systems need not be confluent [Hue80]; on the other hand, strongly non-overlapping right-ground systems are [OO93].

Remark

A partial positive solution is given in [OOTar][TO94], namely, any strongly non-overlapping right-linear term-rewriting system is confluent if it satisfies the condition that for any rewrite rule, no variables occurring more than once in the left-hand-side occur in the right-hand-side.

References

[Che81]
Paul Chew. Unique normal forms in term rewriting systems with repeated variables. In Proceedings of the Thirteenth Annual Symposium on Theory of Computing, pages 7–18. ACM, 1981.
[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.
[OO93]
Michio Oyamaguchi and Yoshikatsu Ohta. On the confluent property of right-ground term rewriting systems. Trans. IEICE, J76-D-I:39–45, 1993.
[OOTar]
Yoshikatsu Ohta, Michio Oyamaguchi, and Yoshihito Toyama. On the Church-Rosser property of simple-right-linear term rewriting systems. Trans. IEICE, to appear.
[TO94]
Yoshihito Toyama and Michio Oyamaguchi. Church-Rosser property and unique normal form property of non-duplicating term rewriting systems. In Nachum Dershowitz and N. Lindenstrauss, editors, Proceedings of the Fourth International Workshop on Conditional Rewriting Systems, Jerusalem, Israel, July 1994. Springer-Verlag.

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