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
Higher-Order and Symbolic Computation, Springer Verlag, 2006
Liste complète des métadonnées

https://hal.inria.fr/inria-00110869
Contributor : Horatiu Cirstea <>
Submitted on : Thursday, November 2, 2006 - 11:02:11 AM
Last modification on : Tuesday, October 25, 2016 - 5:00:21 PM

Identifiers

  • HAL Id : inria-00110869, version 1

Collections

Citation

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>

Share

Metrics

Consultations de la notice

68