Dependency Pairs for Rewriting With Built-in Numbers and Semantic Data Structures
Source: University of New Mexico
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.