The Rewriting Calculus - Part I

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. In this first part, the calculus is motivated and its syntax and evaluation rules for any theory T are presented. In the syntactic case, i.e. when T is the empty theory, we study its basic properties for the untyped case. We first show how it uniformly encodes lambda-calculus as well as first-order rewriting derivations. Then we provide sufficient conditions for ensuring confluence of the calculus.
Type de document :
Article dans une revue
Logic Journal of the Interest Group in Pure and Applied Logics, 2001, 9 (3), pp.427-463
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-00100531, version 1



Horatiu Cirstea, Claude Kirchner. The Rewriting Calculus - Part I. Logic Journal of the Interest Group in Pure and Applied Logics, 2001, 9 (3), pp.427-463. 〈inria-00100531〉



Consultations de la notice