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 in rewriting increases the expressive power of rules 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 an inductive proof method for termination of priority rewriting, relying on an explicit induction on the termination property and working by generating proof trees, which model the rewriting relation by using abstraction and narrowing.
Type de document :
Communication dans un congrès
Adrian Horia Dediu and Armand Mihai Ionescu and Carlos Martin-Vide. Third International Conference on Language and Automata Theory and Applications - LATA 2009, Apr 2009, Tarragona, Spain. Springer, 5457, pp.386-397, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-00982-2_33〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00428679
Contributeur : Isabelle Gnaedig <>
Soumis le : jeudi 29 octobre 2009 - 13:00:21
Dernière modification le : jeudi 11 janvier 2018 - 06:21:25

Lien texte intégral

Identifiants

Collections

Citation

Isabelle Gnaedig. Termination of Priority Rewriting. Adrian Horia Dediu and Armand Mihai Ionescu and Carlos Martin-Vide. Third International Conference on Language and Automata Theory and Applications - LATA 2009, Apr 2009, Tarragona, Spain. Springer, 5457, pp.386-397, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-00982-2_33〉. 〈inria-00428679〉

Partager

Métriques

Consultations de la notice

184