Dependency Pairs for Rewriting With Built-in Numbers and Semantic Data Structures

This paper defines an expressive class of constrained equational rewrite systems that supports the use of semantic data structures (e.g., sets or multisets) and contains built-in numbers, thus extending the previous work presented at CADE 2007. These rewrite systems, which are based on normalized rewriting on constructor terms, allow the specification of algorithms in a natural and elegant way. Built-in numbers are helpful for this since numbers are a primitive data type in every programming language. The authors develop a dependency pair framework for these rewrite systems, resulting in a flexible and powerful method for showing termination that can be automated effectively.