Skip to Main content Skip to Navigation
Journal articles

Expressing Combinatory Reduction Systems Derivations in the Rewriting Calculus

Horatiu Cirstea 1 Clara Bertolissi 1 Claude Kirchner 1 
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Document type :
Journal articles
Complete list of metadata
Contributor : Horatiu Cirstea Connect in order to contact the contributor
Submitted on : Thursday, November 2, 2006 - 11:02:11 AM
Last modification on : Friday, February 4, 2022 - 3:23:16 AM


  • HAL Id : inria-00110869, version 1



Horatiu Cirstea, Clara Bertolissi, Claude Kirchner. Expressing Combinatory Reduction Systems Derivations in the Rewriting Calculus. Higher-Order and Symbolic Computation, Springer Verlag, 2006. ⟨inria-00110869⟩



Record views