Sciweavers

Share
WFLP
2009
Springer

Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures

10 years 4 months ago
Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
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 contextsensitive 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 su...
Stephan Falke, Deepak Kapur
Added 25 May 2010
Updated 25 May 2010
Type Conference
Year 2009
Where WFLP
Authors Stephan Falke, Deepak Kapur
Comments (0)
books