Skip to Main content Skip to Navigation
Reports

Termination of Priority Rewriting - Extended version

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.
Document type :
Reports
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/inria-00349031
Contributor : Isabelle Gnaedig <>
Submitted on : Tuesday, March 31, 2009 - 9:32:50 PM
Last modification on : Tuesday, December 18, 2018 - 4:48:02 PM
Long-term archiving on: : Saturday, November 26, 2016 - 7:02:22 AM

File

version-hal-lata.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00349031, version 2

Collections

Citation

Isabelle Gnaedig. Termination of Priority Rewriting - Extended version. [Research Report] 2008. ⟨inria-00349031v2⟩

Share

Metrics

Record views

300

Files downloads

158