Problem #61 (Solved !)
Originator: Tobias Nipkow, Masako Takahashi
Date: June 1993
Summary:
Are weakly orthogonal higher-order rewrite systems confluent?
For higher-order rewrite formats as given by combinatory
reduction systems [Klo80] and higher-order rewrite systems
[Nip91, Tak93],
confluence has been proved in the restricted case of
orthogonal systems. Can confluence be extended to
such systems when they are weakly orthogonal (all critical pairs are trivial)?
When critical pairs arise only at the root,
confluence is known to hold.
Remark
Weakly orthogonal higher-order rewriting systems are confluent.
This has been shown both via the Tait-Martin-Löf method and
via finite developments [vOvR94].
The details and further extensions similar to Huet’s parallel closure
condition can be found in [Oos94, Oos97, Raa96].
References
-
[Klo80]
-
Jan Willem Klop.
Combinatory Reduction Systems, volume 127 of Mathematical
Centre Tracts.
Mathematisch Centrum, Amsterdam, 1980.
- [Nip91]
-
Tobias Nipkow.
Higher-order critical pairs.
In Gilles Kahn, editor, Sixth
Symposium on Logic in
Computer Science, pages 342–349, Amsterdam, The Netherlands, July 1991.
IEEE.
- [Oos94]
-
Vincent van Oostrom.
Confluence for Abstract and Higher-Order Rewriting.
PhD thesis, Vrije Universiteit, Amsterdam, 1994.
- [Oos97]
-
Vincent van Oostrom.
Developing developments.
Theoretical Computer
Science, 175:159–181, 1997.
- [Raa96]
-
Femke van Raamsdonk.
Confluence and Normalization for Higher-Order Rewriting.
PhD thesis, Vrije Universiteit, Amsterdam, 1996.
- [Tak93]
-
Masako Takahashi.
λ-calculi with conditional rules.
In M. Bezem and J. F. Groote, editors, Proceedings of the
International Conference on Typed Lambda Calculi and Applications (Utrecht,
The Netherlands), volume 664 of Lecture Notes in Computer
Science, pages 406–417, Berlin, 1993.
Springer-Verlag.
- [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.