Proving Weak Properties of Rewriting

Isabelle Gnaedig 1 Hélène Kirchner 2
1 CARTE - Theoretical adverse computations, and safety
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : In rule-based programming, properties of programs, such as termination, are in general considered in their strong acceptance i.e., on every computation branch. But in practice, they may hold in their weak acceptance only i.e., on at least one computation branch. Moreover, weak properties are often enough to ensure that programs give the expected result. There are very few results to handle weak properties of rewriting. We address here two of them: termination and reducibility to a constructor form, in a unified framework allowing us to prove them inductively. Proof trees are developed, which simulate rewriting trees by narrowing and abstracting subterms. Our technique is constructive in the sense that proof trees can be used to infer an evaluation strategy for any given input: the right computation branch is developed without using a costly breadth-first strategy nor backtracking.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2011, 412, pp.4405-4438. 〈10.1016/j.tcs.2011.04.028〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00592271
Contributeur : Isabelle Gnaedig <>
Soumis le : vendredi 14 septembre 2018 - 14:10:03
Dernière modification le : vendredi 21 septembre 2018 - 17:15:43

Fichier

weak-tcs-revision2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Isabelle Gnaedig, Hélène Kirchner. Proving Weak Properties of Rewriting. Theoretical Computer Science, Elsevier, 2011, 412, pp.4405-4438. 〈10.1016/j.tcs.2011.04.028〉. 〈inria-00592271〉

Partager

Métriques

Consultations de la notice

275

Téléchargements de fichiers

19