Paper Info
Title
Dependency Pairs for Rewriting with Non-free Constructors
Abstract
A method based on dependency pairs for showing termination of functional programs on data structures generated by constructors with relations is proposed. A functional program is specified as an equational rewrite system, where the rewrite system specifies the program and the equations express the relations on the constructors that generate the data structures. Unlike previous approaches, relations on constructors can be collapsing, including idempotency and identity relations. Relations among constructors may be partitioned into two parts: (i) equations that cannot be oriented into terminating rewrite rules, and (ii) equations that can be oriented into terminating rewrite rules, in which case an equivalent convergent system for them is generated. The dependency pair method is extended to normalized rewriting, where constructor-terms in the redex are normalized first. The method has been applied to several examples, including the Calculus of Communicating Systems and the Propositional Sequent Calculus. Various refinements, such as dependency graphs, narrowing, etc., which increase the power of the dependency pair method, are presented for normalized rewriting.
Year
DOI
Venue
2007
10.1007/978-3-540-73595-3_32
CADE
Keywords
Field
DocType
dependency pairs,dependency pair method,equivalent convergent system,functional program,communicating systems,dependency pair,non-free constructors,identity relation,dependency graph,propositional sequent calculus,previous approach,data structure,functional programming,calculus of communicating systems,sequent calculus
Data structure,Discrete mathematics,Dependency pairs,Normalization (statistics),Computer science,Sequent calculus,Algorithm,Normalization property,Rewriting,Idempotence,Dependency graph
Conference
Volume
ISSN
Citations 
4603
0302-9743
4
PageRank 
References 
Authors
0.42
18
2
Name
Order
Citations
PageRank
Stephan Falke151127.86
Deepak Kapur22282235.00