Confluence and superdevelopments

Abstract

In this paper a short proof is presented for confluence of a quite general class of reduction systems, containing λ-calculus and term rewrite systems: the orthogonal combinatory reduction systems. Combinatory reduction systems (CRSs for short) were introduced by Klop generalizing an idea of Aczel. In CRSs, the usual first-order term rewriting format is extended with binding structures for variables. This permits to express besides first order term rewriting also λ-calculus, extensions of λ-calculus and proof normalizations. Confluence will be proved for orthogonal CRSs, that is, for those CRSs having left-linear rules and no critical pairs. The proof proceeds along the lines of the proof of Tait and Martin-Löf for confluence of λ-calculus, but uses a different notion of ”parallel reduction” as employed by Aczel. It gives rise to an extended notion of development, called ”superdevelopment”. A superdevelopment is a reduction sequence in which besides redexes that descend from the initial term also some redexes that are created during reduction may be contracted. For the case of λ-calculus, all superdevelopments are proved to be finite. A link with the confluence proof is provided by proving that superdevelopments characterize exactly the Aczel's notion of ”parallel reduction” used in order to obtain confluence.

supported by NWO/SION project 612-316-606 Extensions of orthogonal rewrite systems — syntactic properties.