The Rewriting Calculus as a Combinatory Reduction System

The last few years have seen the development of the rewriting calculus (also called rho-calculus or ρ-calculus) that uniformly integrates first-order term rewriting and λ-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 Combinatory Reduction Systems (crs), or by adding to λ-calculus algebraic features. In a previous work, the authors showed how the semantics of crs can be expressed in terms of the ρ-calculus. 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.

• Type: Conference
• Year: 2007
• Where: FOSSACS
• Authors: Clara Bertolissi, Claude Kirchner
• Keywords: Applied Computing, Combinatory Reduction Systems, FOSSACS 2007, Rewriting Calculus, Term Rewriting