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.
Partially supported by NSF grant CCF-0541315.