Paper Info
Title
Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
Abstract
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.
Year
DOI
Venue
2008
10.1007/978-3-540-70590-1_7
RTA
Keywords
Field
DocType
dependency pairs,expressive class,reduction pair,powerful method,successful automatic termination proof,semantic data structures,built-in numbers,various powerful technique,built-in number,semantic data structure,dependency pair framework,constructor term,primitive data type,data type,power method,programming language,data structure
Dependency pairs,Normalization (statistics),Programming language,Computer science,Algorithm,Theoretical computer science,Rewriting,Primitive data type,Semantic data model
Conference
Volume
ISSN
Citations 
5117
0302-9743
12
PageRank 
References 
Authors
0.65
24
2
Name
Order
Citations
PageRank
Stephan Falke151127.86
Deepak Kapur22282235.00