Dependency Pairs for Rewriting with Non-Free Constructors

 

Stefan Falke (University of New Mexico at Albuquerque)

 

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.