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].
Remark
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].
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.
- [Klo80]
-
Jan Willem Klop.
Combinatory Reduction Systems, volume 127 of Mathematical
Centre Tracts.
Mathematisch Centrum, Amsterdam, 1980.
- [MO94]
-
K. Mano and M. Ogawa.
A new proof of Chew’s theorem.
Technical report, IPSJ PRG94-19-7, 1994.
- [MR84]
-
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.
- [Ohl94]
-
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.
- [OO89]
-
M. Ogawa and S. Ono.
On the uniquely converging property of nonlinear term rewriting
systems.
Technical report, IEICE COMP89-7, 1989.
- [OO93]
-
Michio Oyamaguchi and Yoshikatsu Ohta.
On the confluent property of right-ground term rewriting systems.
Trans. IEICE, J76-D-I:39–45, 1993.
- [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.
- [Ver96]
-
Rakesh M. Verma.
Unicity and modularity of confluence for term rewriting systems.
Technical report, University of Houston, 1996.
- [Ver97]
-
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.