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

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.


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].


Jan Willem Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1980.
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.
Vincent van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1994.
Vincent van Oostrom. Developing developments. Theoretical Computer Science, 175:159–181, 1997.
Femke van Raamsdonk. Confluence and Normalization for Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1996.
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.
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.

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