Skip to Main content Skip to Navigation
Reports

Termination of Priority Rewriting

Isabelle Gnaedig 1
1 CARTE - Theoretical adverse computations, and safety
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est
Abstract : Introducing priorities on rules in rewriting increases their expressive power 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 in this paper an inductive proof method for termination of priority rewriting, relying on an explicit induction on the termination property. It works by generating proof trees, modeling the rewriting relation by using abstraction and narrowing. As it specifically handles priorities on the rules, our technique allows proving termination of term rewrite systems that would diverge without priorities.
Document type :
Reports
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/inria-00243131
Contributor : Isabelle Gnaedig <>
Submitted on : Friday, May 23, 2008 - 10:53:58 AM
Last modification on : Tuesday, December 18, 2018 - 4:48:02 PM
Long-term archiving on: : Thursday, September 27, 2012 - 5:51:18 PM

File

IP-termin-hal.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00243131, version 1

Collections

Citation

Isabelle Gnaedig. Termination of Priority Rewriting. [Research Report] 2008, pp.13. ⟨inria-00243131⟩

Share

Metrics

Record views

253

Files downloads

166