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...

• Type: Conference
• Year: 2009
• Where: WFLP
• Authors: Stephan Falke, Deepak Kapur
• Keywords: Algorithms, Context-sensitive Rewriting, Contextsensitive Rewriting, Several Powerful Termination, WFLP 2009