Stephan Falke and Deepak Kapur:
Dependency Pairs for Rewriting with Non-Free Constructors
Technical Report TR-CS-2007-07, Department of Computer Science, University of New Mexico, Albuquerque, NM, USA, 2007.
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 as
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.
[
BibTeX
|
Paper (ps.gz)
|
Paper (pdf)
]