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.
dvi
At Springer:
http://dx.doi.org/10.1007/BFb0037114
BibTeX:
@inproceedings{Nipkow-TLCA-93,
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",
pages="306--317",series=LNCS,volume=664,publisher=Springer,year=1993}
A much extended journal article
appeared in Theoretical Computer Science.