Expressing combinatory reduction systems derivations in the rewriting calculus

摘要

The last few years have seen the development of the rewriting calculus (also called rho-calculus or ρ-calculus) that uniformly integrates first-order term rewriting and the λ-calculus. The combination of these two latter formalisms has been already handled either by enriching first-order rewriting with higher-order capabilities, like in the Combinatory Reduction Systems (CRS), or by adding to the λ-calculus algebraic features. The various higher-order rewriting systems and the rewriting calculus share similar concepts and have similar applications, and thus, it is important to compare these formalisms to better understand their respective strengths and differences. 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 ρ-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.