The Rewriting Calculus - Part II

Horatiu Cirstea 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 : The rho-calculus integrates in a uniform and simple setting first-order rewriting, lambda-calculus and non-deterministic computations. Its abstraction mechanism is based on the rewrite rule formation and its main evaluation rule is based on matching modulo a theory T. We have seen in the first part of this work the motivations, definitions and basic properties of the rho-calculus. This second part is first devoted to the use of an extension of the rho-calculus for encoding a (conditional) rewrite relation. This extension is based on the ``first'' operator whose purpose is to detect rule application failure. It allows us to express recursively rule application and therefore to encode strategy based rewriting processes. We then use this extended calculus to give an operational semantics to ELAN programs. We conclude with an overview of ongoing and future works on rho-calculus.
Type de document :
Article dans une revue
Logic Journal of the Interest Group in Pure and Applied Logics, 2001, 9 (3), pp.465-498
Liste complète des métadonnées
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:46:31
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57


  • HAL Id : inria-00100532, version 1



Horatiu Cirstea, Claude Kirchner. The Rewriting Calculus - Part II. Logic Journal of the Interest Group in Pure and Applied Logics, 2001, 9 (3), pp.465-498. 〈inria-00100532〉



Consultations de la notice