| Weak Orthogonality Implies Confluence: the Higher-Order Case (1994) | |||||||||||||||||||
Abstract | |||||||||||||||||||
| In this paper we prove confluence for weakly orthogonal Higher-Order Rewriting Systems. This generalises all the known `confluence by orthogonality' results. AMS Subject Classification (1991): 68Q50 CR Subject Classification (1991): F.4.1, F.3.3 Keywords & Phrases: higher-order rewriting, weak orthogonality, confluence. Note: Most of the research of the first author has been carried out during his employment at the Vrije Universiteit, Amsterdam, The Netherlands. The research of the second author is supported by NWO/SION project 612-316-606. 1. Introduction This paper deals with higher-order term rewriting. Since our approach of higher-order term rewriting is different from the usual one, both in respect to the concept of `higher-order' and to the notion of `term rewriting', we first comment on our approach and the terminology used, before stating the general confluence result. term rewriting. In term rewriting as usually defined (see e.g. [DJ89, Klo92, Klo80, Nip91]) rewrite steps... | |||||||||||||||||||
Details der Publikation | |||||||||||||||||||
| |||||||||||||||||||