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 on rules increases the expressive power of rewriting and helps to limit computations. Priority rewriting is used as a com- putation model for the functional paradigm. Termination of priority rewriting then warrants that programs give a result. We describe in this paper an induc- tive proof method for termination of priority rewriting, lying on an inductive mechanism on the termination property. It works by generating proof trees, using abstraction and narrowing. As it specifically handles priorities on the rules, our technique allows proving termination of rewrite systems that would diverge without priorities.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00349031
Contributor : Isabelle Gnaedig Connect in order to contact the contributor
Submitted on : Sunday, March 22, 2009 - 7:00:04 AM
Last modification on : Saturday, October 16, 2021 - 11:26:05 AM
Long-term archiving on: : Thursday, October 11, 2012 - 2:50:58 PM

File

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

Identifiers

  • HAL Id : inria-00349031, version 1

Citation

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

Share

Metrics

Les métriques sont temporairement indisponibles