Combinatory Reduction Systems, or CRSs for short, 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. Bound variables are also present in many other rewrite systems, such as systems with simplification rules for proof normalization. The original idea of CRSs is due to Aczel, who introduced a restricted class of CRSs and, under the assumption of orthogonality, proved confluence. Orthogonality means that the rules are non-ambiguous (no overlap leading to a critical pair) and left-linear (no global comparison of terms necessary).
We introduce the class of orthogonal CRSs, illustrated with many examples, discuss its expressive power, and give an outline of a short proof of confluence. This proof is a direct generalization of Aczel's original proof, which is close to the well-known confluence proof for lambda-calculus by Tait and Martin-Löf. There is a well-known connection between the parallel reduction featuring in the latter proof, 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' used in Aczel's proof gives rise to a generalized form of developments, which we call `superdevelopments' and on which we will briefly comment.
We conclude with 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).