Orthogonal Higher-Order Rewrite Systems are Confluent

Tobias Nipkow

Higher-order rewrite systems (HRS) are rewrite systems over simply typed lambda-terms with restricted left-hand sides. They were introduced by Nipkow [LICS91] where it was shown that the notion of critical pairs generalizes to HRS. This paper is a second step towards a general theory of higher-order rewrite systems. It considers the complementary case, when there are no critical pairs, all rules are left-linear (no free variable appears twice on the left-hand side), and termination is immaterial. Such systems are usually called orthogonal. The main result of this paper is that all orthogonal HRS are confluent.


At Springer: http://dx.doi.org/10.1007/BFb0037114


author="Tobias Nipkow",
title="Orthogonal Higher-Order Rewrite Systems are Confluent",
booktitle="Proc.\ Int.\ Conf.\ Typed Lambda Calculi and Applications",
editor="M. Bezem and J.F. Groote",
A much extended journal article appeared in Theoretical Computer Science.