The Rewriting Calculus as a Combinatory Reduction System
Résumé
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.