Orthogonal Higher-Order Rewrite Systems are Confluent
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.
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.