Developments in the rewriting calculus - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2006

Developments in the rewriting calculus

Résumé

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.
Fichier principal
Vignette du fichier
paper.pdf (209.01 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00121212 , version 1 (19-12-2006)
inria-00121212 , version 2 (08-01-2007)
inria-00121212 , version 3 (12-01-2007)

Identifiants

  • HAL Id : inria-00121212 , version 1

Citer

Clara Bertolissi. Developments in the rewriting calculus. [Research Report] 2006. ⟨inria-00121212v1⟩
56 Consultations
50 Téléchargements

Partager

Gmail Facebook X LinkedIn More