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 “occurcheck” [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 PRG94197, 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 constructorsharing 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.
SpringerVerlag.
 [OO89]

M. Ogawa and S. Ono.
On the uniquely converging property of nonlinear term rewriting
systems.
Technical report, IEICE COMP897, 1989.
 [OO93]

Michio Oyamaguchi and Yoshikatsu Ohta.
On the confluent property of rightground term rewriting systems.
Trans. IEICE, J76DI:39–45, 1993.
 [TO94]

Yoshihito Toyama and Michio Oyamaguchi.
ChurchRosser property and unique normal form property of
nonduplicating term rewriting systems.
In Nachum Dershowitz and N. Lindenstrauss, editors, Proceedings
of the Fourth International Workshop on Conditional Rewriting Systems,
Jerusalem, Israel, July 1994.
SpringerVerlag.
 [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. SpringerVerlag, September 1997.