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
Liste complète des métadonnées
Contributor : Horatiu Cirstea <>
Submitted on : Thursday, November 2, 2006 - 11:02:11 AM
Last modification on : Thursday, January 11, 2018 - 6:19:57 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