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 our previous work presented at CADE 2007 [6]. 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. We develop a dependency pair framework for these rewrite systems, resulting in a flexible and powerful method for showing termination that can be automated effectively. Various powerful techniques are developed within this framework, including a subterm criterion and reduction pairs that need to consider only subsets of the rules and equations. It is well-known from the dependency pair framework for ordinary rewriting that these techniques are often crucial for a successful automatic termination proof. Termination of a large collection of examples can be established using the presented techniques. © 2008 Springer-Verlag.
CITATION STYLE
Falke, S., & Kapur, D. (2008). Dependency pairs for rewriting with built-in numbers and semantic data structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5117 LNCS, pp. 94–109). https://doi.org/10.1007/978-3-540-70590-1_7
Mendeley helps you to discover research relevant for your work.