Combinatory Reduction Systems (CRSs) were designed to combine the usual first-order format of term rewriting with the presence of bound variables as in pure lambda-calculus and various typed lambda-calculi. The paper introduces the class of orthogonal CRSs, illustrated with many examples, discusses its expressive power, and gives an outline of a short proof of confluence. There is a well-known connection between the parallel reduction and the concept of 'developments', and a classical lemma in the theory of lambda-calculus is that of 'Finite Developments', a strong normalization result. It turns out that the notion of 'parallel reduction' gives rise to a generalized form of developments, called 'superdevelopments' and on which it briefly comments. It concludes by mentioning the results of a comparison of CRSs with the recently proposed and strongly related format of higher-order rewriting: Nipkow's HRSs (Higher-order Rewrite Systems).
展开▼
