MOVES Seminar, 10 July 2008
Two talks for the price of none!
PART I: Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures
PART II: Dependency Pairs for Rewriting with Built-in Numbers and Semantic Data Structures
Stephan Falke (University of New Mexico at Albuquerque)
Abstract:
I.
While ordinary conditional rewrite systems are more elegant than unconditional
ones, they still have limited expressive power since semantic data structures
such as sets or multisets cannot be modeled elegantly. This talk presents
a class of conditional rewrite systems that allows the use of semantic data
structures and supports built-in natural numbers, including constraints taken
from Presburger arithmetic. The framework is both expressive and natural.
Rewriting is performed using a combination of normalized equational rewriting
with recursive evaluation of conditions and validity checking of instantiated
constraints. Termination is one of the most important properties of rewriting.
For conditional systems, it is not sufficient to only show well-foundedness
of the rewrite relation, but it also has to be ensured that evaluation of the
conditions terminates. These properties are captured by the notion of
operational termination. In this work, we show that operational termination
for the class of conditional rewrite systems discussed above can be reduced to
(regular) termination of unconditional systems using a syntactic
transformation. Powerful methods for showing termination of unconditional
systems are presented in the second part.
ones, they still have limited expressive power since semantic data structures
such as sets or multisets cannot be modeled elegantly. This talk presents
a class of conditional rewrite systems that allows the use of semantic data
structures and supports built-in natural numbers, including constraints taken
from Presburger arithmetic. The framework is both expressive and natural.
Rewriting is performed using a combination of normalized equational rewriting
with recursive evaluation of conditions and validity checking of instantiated
constraints. Termination is one of the most important properties of rewriting.
For conditional systems, it is not sufficient to only show well-foundedness
of the rewrite relation, but it also has to be ensured that evaluation of the
conditions terminates. These properties are captured by the notion of
operational termination. In this work, we show that operational termination
for the class of conditional rewrite systems discussed above can be reduced to
(regular) termination of unconditional systems using a syntactic
transformation. Powerful methods for showing termination of unconditional
systems are presented in the second part.
II.
This talk defines an expressive class of constrained equational rewrite systems
that supports the use of semantic data structures (e.g., sets or multisets)
and contains built-in numbers. These rewrite systems, which are based on
normalized rewriting on constructor terms, allow the specification of
algorithms in a natural and elegant way. Built-in numbers are helpful for this
since numbers are a primitive data type in every programming language. We
develop a dependency pair framework for these rewrite systems, resulting in a
flexible and powerful method for showing termination that can be automated
effectively. Various powerful techniques are developed within this framework,
including a subterm criterion and reduction pairs that need to consider only
subsets of the rules and equations. It is well-known from the dependency pair
framework for ordinary rewriting that these techniques are often crucial for a
successful automatic termination proof.
that supports the use of semantic data structures (e.g., sets or multisets)
and contains built-in numbers. These rewrite systems, which are based on
normalized rewriting on constructor terms, allow the specification of
algorithms in a natural and elegant way. Built-in numbers are helpful for this
since numbers are a primitive data type in every programming language. We
develop a dependency pair framework for these rewrite systems, resulting in a
flexible and powerful method for showing termination that can be automated
effectively. Various powerful techniques are developed within this framework,
including a subterm criterion and reduction pairs that need to consider only
subsets of the rules and equations. It is well-known from the dependency pair
framework for ordinary rewriting that these techniques are often crucial for a
successful automatic termination proof.
