The Rewriting Calculus as a Combinatory Reduction System

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 : rewriting calculus CRS
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00121792
Contributor : Claude Kirchner <>
Submitted on : Friday, December 22, 2006 - 9:37:18 AM
Last modification on : Friday, March 9, 2018 - 11:25:15 AM

Links full text

Identifiers

Collections

Citation

Clara Bertolissi, Claude Kirchner. The Rewriting Calculus as a Combinatory Reduction System. Tenth International Conference on Foundations of Software Science and Computations Structures - FoSSaCS 2007, Mar 2007, Braga, Portugal. pp.78-92, ⟨10.1007/978-3-540-71389-0_7⟩. ⟨inria-00121792⟩

Share

Metrics

Record views

197