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

Problem #79

Originator: Mizuhito Ogawa
Date: April 1995

Summary: Does a system that is nonoverlapping under unification with infinite terms have unique normal forms?

Does a system that is nonoverlapping under unification with infinite terms (unification without “occur-check” [MR84]) have unique normal forms? This conjecture was originally proposed in [OO89] with an incomplete proof, as an extension of the result on strongly nonoverlapping systems [Klo80][Che81]. Related results appear in [OO93][TO94][MO94], but the original conjecture is still open. This is related to Problem 58. This problem is also related with modularity of confluence of systems sharing constructors, see [Ohl94].


The answer is yes if the system is also nonduplicating [Ver96]. A direct technique is given in [Ver96]. The nonduplicating condition can be relaxed under a certain technical condition [Ver96]. Some extensions to handle root overlaps are given in [Ver97] and a restricted version of the result in [Che81] is also proved using the direct technique in [Ver97].


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.
Jan Willem Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1980.
K. Mano and M. Ogawa. A new proof of Chew’s theorem. Technical report, IPSJ PRG94-19-7, 1994.
A. Martelli and G. Rossi. Efficient unification with infinite terms in logic programming. In International conference on fifth generation computer systems, pages 202–209, 1984.
Enno Ohlebusch. On the modularity of confluence of constructor-sharing term rewriting systems. In Sophie Tison, editor, Colloquium on Trees in Algebra and Programming, volume 787 of Lecture Notes in Computer Science, Edinburgh, Scotland, 1994. Springer-Verlag.
M. Ogawa and S. Ono. On the uniquely converging property of nonlinear term rewriting systems. Technical report, IEICE COMP89-7, 1989.
Michio Oyamaguchi and Yoshikatsu Ohta. On the confluent property of right-ground term rewriting systems. Trans. IEICE, J76-D-I:39–45, 1993.
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.
Rakesh M. Verma. Unicity and modularity of confluence for term rewriting systems. Technical report, University of Houston, 1996.
Rakesh M. Verma. Unique normal forms for nonlinear term rewriting systems: Root overlaps. In Symp. on Fundamentals of Computation Theory, volume 1279 of Lecture Notes in Computer Science, pages 452–462. Springer-Verlag, September 1997.

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