Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Proving weak properties of rewriting

Isabelle Gnaedig 1, * Hélène Kirchner 1, 2 
* Corresponding author
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.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Isabelle Gnaedig Connect in order to contact the contributor
Submitted on : Tuesday, November 11, 2008 - 9:03:38 PM
Last modification on : Thursday, October 27, 2022 - 4:02:27 AM


  • HAL Id : inria-00338181, version 1


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



Record views