Skip to Main content Skip to Navigation
Reports

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.
Complete list of metadatas

https://hal.inria.fr/inria-00338181
Contributor : Isabelle Gnaedig <>
Submitted on : Tuesday, November 11, 2008 - 9:03:38 PM
Last modification on : Tuesday, December 18, 2018 - 4:48:02 PM

Identifiers

  • HAL Id : inria-00338181, version 1

Collections

Citation

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

Share

Metrics

Record views

230