| Combinatory reduction systems: Introduction and survey (1993) | |||||||||||||||
Abstract | |||||||||||||||
| 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-calculus and various typed-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-calculus by Tait and Martin-Lof. 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-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 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||