Stephan Falke

 

(University of New Mexico, Albuquerque, NM, USA)

 

Dependency Pairs for Rewriting with Built-in Numbers and Semantic Data Structures

 

Rewrite systems on free data structures have limited expressive power
since semantic data structures like sets or multisets cannot be
modeled elegantly. In this work we define a class of rewrite systems
that allows the use of semantic data structures. Additionally,
built-in natural numbers, including (dis)equality, ordering, and
divisibility constraints, are supported. The rewrite mechanism is a
combination of normalized equational rewriting with validity checking
of instantiated constraints.  The framework is highly expressive and
allows modeling of algorithms in a natural way.

Termination is one of the most important properties of
algorithms. This is true for both functional programs and imperative
programs operating on natural numbers, which can be translated into
rewrite systems. In this work, the dependency pair framework for
proving termination is extended to be applicable to the class of
rewrite systems described above, thus obtaining a flexible and
powerful method for showing termination that can be automated
effectively. We develop various refinements which increase power and
efficiency of the method.