# The Rewriting Calculus as a Combinatory Reduction System

2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The last few years have seen the development of the \emph{rewriting calculus} (also called rho-calculus or \RHO) that uniformly integrates first-order term rewriting and $\lambda$-calculus. The combination of these two latter formalisms has been already handled either by enriching first-order rewriting with higher-order capabilities, like in the \emph{Combinatory Reduction Systems} (\CRS), or by adding to $\lambda$-calculus algebraic features. In a previous work, the authors showed how the semantics of \CRS\ can be expressed in terms of the \RHO. The converse issue is adressed here: rewriting calculus derivations are simulated by Combinatory Reduction Systems derivations. As a consequence of this result, important properties, like standardisation, are deduced for the rewriting calculus.
Keywords :
Type de document :
Communication dans un congrès
Helmut Seidl. Tenth International Conference on Foundations of Software Science and Computations Structures - FoSSaCS 2007, Mar 2007, Braga, Portugal. Springer-Verlag, 4423, pp.78-92, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-71389-0_7〉

https://hal.inria.fr/inria-00121792
Contributeur : Claude Kirchner <>
Soumis le : vendredi 22 décembre 2006 - 09:37:18
Dernière modification le : vendredi 9 mars 2018 - 11:25:15

### Citation

Clara Bertolissi, Claude Kirchner. The Rewriting Calculus as a Combinatory Reduction System. Helmut Seidl. Tenth International Conference on Foundations of Software Science and Computations Structures - FoSSaCS 2007, Mar 2007, Braga, Portugal. Springer-Verlag, 4423, pp.78-92, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-71389-0_7〉. 〈inria-00121792〉

### Métriques

Consultations de la notice