Developments in the rewriting calculus

Abstract : The theory of developments, originally developed for the Lambda calculus, has been successfully adapted to several other computational paradigms, like first- and higher-order term rewrite system. The main desirable results on developments are the fact that the complete development of a finite set of redexes always terminates (FD) and the fact that, for a given initial term, all complete developments of a fixed set of redexes end with the same term (FD!). Following the ideas in the Lambda calculus, in this paper, we present a notion of development and the proofs of theorems FD and FD! for the rewriting calculus, a framework embedding Lambda calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. As an additional contribution, a new proof of the confluence property for the rewriting calculus, is obtained as a consequence of the results on developments.
Type de document :
[Research Report] 2006
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger
Contributeur : Clara Bertolissi <>
Soumis le : vendredi 12 janvier 2007 - 16:43:41
Dernière modification le : vendredi 9 mars 2018 - 11:24:29
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 14:13:12


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00121212, version 3



Clara Bertolissi. Developments in the rewriting calculus. [Research Report] 2006. 〈inria-00121212v3〉



Consultations de la notice


Téléchargements de fichiers