Stephan Falke and Deepak Kapur:
Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
Technical Report TR-CS-2009-01, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2009.
Context-sensitive rewriting is a restriction of rewriting that can be used to
elegantly model declarative specification and programming languages such as
Maude. Furthermore, it can be used to model lazy evaluation in functional
languages such as Haskell. Building upon our previous work on an expressive
and elegant class of rewrite systems (called CERSs) that contains built-in
numbers and supports the use of collection data structures such as sets or
multisets, we consider context-sensitive rewriting with CERSs in this paper.
This integration results in a natural way for specifying algorithms in the
rewriting framework. In order to prove termination of this kind of
rewriting automatically, we develop a dependency pair framework for
context-sensitive rewriting with CERSs, resulting in a flexible termination
method that can be automated effectively. Several powerful termination
techniques are developed within this framework. An implementation in the
termination prover AProVE has been successfully evaluated on a large
collection of examples.
[
BibTeX
|
Paper (ps.gz)
|
Paper (pdf)
|
Erratum (ps.gz)
|
Erratum (pdf)
]