Stephan Falke and Deepak Kapur
Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
In Proceedings of the 18th International Workshop on Functional and (Constraint) Logic Programming (WFLP '09), Brasília, Brazil.
Workshop Proceedings, pages 111-125, 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
automatically prove termination of this kind of rewriting, 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)
]