Termination of Priority Rewriting

14 years 1 months ago
Termination of Priority Rewriting
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. Categories and Subject Descriptors F.3.1 [LOGICS AND MEANINGS OF PROGRAMS]: Specifying and Verifying and Reasoning about Programs—Logics of programs, Mechanical verification, Specification techniques; F.4.2 [MATHEMATICAL LOGIC AND FORMAL LANGUAGES]: Grammars and Other Rewriting System...
Isabelle Gnaedig
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Where LATA
Authors Isabelle Gnaedig
Comments (0)