Termination of Priority Rewriting

Isabelle Gnaedig 1
1 CARTE - Theoretical adverse computations, and safety
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Introducing priorities on rules in rewriting increases their expressive power and helps to limit computations. Priority rewriting is used in rule-based programming as well as in functional programming. Termination of priority rewriting is then important to guarantee that programs give a result. We describe in this paper an inductive proof method for termination of priority rewriting, relying on an explicit induction on the termination property. It works by generating proof trees, modeling the rewriting relation by using abstraction and narrowing. As it specifically handles priorities on the rules, our technique allows proving termination of term rewrite systems that would diverge without priorities.
Type de document :
Rapport
[Research Report] 2008, pp.13
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00243131
Contributeur : Isabelle Gnaedig <>
Soumis le : vendredi 23 mai 2008 - 10:53:58
Dernière modification le : mardi 18 décembre 2018 - 16:48:02
Document(s) archivé(s) le : jeudi 27 septembre 2012 - 17:51:18

Fichier

IP-termin-hal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00243131, version 1

Collections

Citation

Isabelle Gnaedig. Termination of Priority Rewriting. [Research Report] 2008, pp.13. 〈inria-00243131〉

Partager

Métriques

Consultations de la notice

223

Téléchargements de fichiers

103