Search

Abstract??The last few years have seen the development of therewriting 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 theCombinatory 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 possibleCRS-reduction into a corresponding ?-reduction. Since for this purpose we need to make precise the matching used when evaluatingCRS, the second contribution of the paper is to present an original matching algorithm forCRSterms that uses a simple term translation and the classical matching of lambda terms.