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 the 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, the authors consider context sensitive rewriting with CERSs in this paper. This integration results in a natural way for specifying algorithms in the rewriting framework.