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.
Type de document :
Article dans une revue
Higher-Order and Symbolic Computation, Springer Verlag, 2006
Liste complète des métadonnées

https://hal.inria.fr/inria-00110869
Contributeur : Horatiu Cirstea <>
Soumis le : jeudi 2 novembre 2006 - 11:02:11
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

91