Expressing Combinatory Reduction Systems Derivations in the Rewriting Calculus
Abstract
We show in this paper that we can express Combinatory Reduction Systems derivations in terms of rewriting calculus derivations. The approach we present is based on a translation of each possible CRS-reduction into a corresponding rho-reduction. Since for this purpose we need to make precise the matching used when evaluating \CRS, the second contribution of the paper is to present an original matching algorithm for CRS terms that uses a simple term translation and the classical matching of lambda terms.