Proving weak properties of rewriting

Isabelle Gnaedig 1, * Hélène Kirchner 1, 2
* Auteur correspondant
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 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: on at least one computation branch. Moreover, weak properties are often enough to ensure that programs give the expected result. Very few results exist to handle weak properties of rewriting. We address here two of them: termination and reducibility to a constructor form, nin a unified framework allowing to develop inductive proofs of the considered properties. Proof trees are developed, which simulate rewriting trees by narrowing and an abstraction mechanism exploiting the induction hypothesis. Our technique is constructive in the sense that proof trees can be used to compute an evaluated form of any given data: the good computation branch is developed without to use a costly breadth-first strategy.
Type de document :
[Research Report] 2009, pp.50
Liste complète des métadonnées
Contributeur : Isabelle Gnaedig <>
Soumis le : mardi 11 novembre 2008 - 21:03:38
Dernière modification le : lundi 17 septembre 2018 - 13:42:01


  • HAL Id : inria-00338181, version 1



Isabelle Gnaedig, Hélène Kirchner. Proving weak properties of rewriting. [Research Report] 2009, pp.50. 〈inria-00338181〉



Consultations de la notice