Problem #61 (Solved !)
Originator: Tobias Nipkow, Masako Takahashi
Date: June 1993
Summary:
Are weakly orthogonal higherorder rewrite systems confluent?
For higherorder rewrite formats as given by combinatory
reduction systems [Klo80] and higherorder 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 higherorder rewriting systems are confluent.
This has been shown both via the TaitMartinLö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.
Higherorder 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 HigherOrder 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 HigherOrder 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.
SpringerVerlag.
 [vOvR94]

Vincent van Oostrom and Femke van Raamsdonk.
Weak orthogonality implies confluence: the higherorder 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.
SpringerVerlag.