The following technical report is available from http://aib.informatik.rwth-aachen.de:
The DP Framework for Proving Termination of Term Rewriting René Thiemann AIB 2007-17
Termination is the fundamental property of a program that for each input, the evaluation will eventually stop and return some output. Although the question whether a given program terminates is undecidable, many techniques have been developed which can be used to answer the question of termination for many programs automatically. Especially, termination of term rewriting is an interesting and widely studied area: Since the basic evaluation mechanism of many programming languages is term rewriting, one can successfully apply the termination techniques for term rewriting to analyze termination of programs automatically. Nevertheless, there still remain many programs that cannot be handled by any current technique that is amenable to automation.
In this thesis, we extend existing techniques and develop new methods for mechanized termination analysis of term rewrite systems. Currently, one of the most powerful techniques is the dependency pair approach. Up to now, it was regarded as one of several possible methods to prove termination. We show that dependency pairs can instead be used as a general concept to integrate arbitrary techniques for termination analysis. In this way, the benefits of different techniques can be combined and their modularity and power are increased significantly. We refer to this new concept as the "dependency pair framework" to distinguish it from the old "dependency pair approach".
Moreover, this framework facilitates the development of new methods for termination analysis. To demonstrate this, we design several novel techniques within the dependency pair framework. They can successfully be applied to prove termination of previously challenging programs. For example, our work describes new ways how to handle programs using accumulators, programs written in higher-order languages, and programs which only terminate w.r.t. a given evaluation strategy. We additionally show how to disprove termination, even under strategies.
All presented techniques are formulated in a uniform setting and are implemented in our fully automated termination prover AProVE. The significance of our results is demonstrated at the annual international Termination Competition, where the leading automated tools try to analyze termination of programs from different areas of computer science: Without the contributions of this thesis, AProVE would not have reached the highest scores both for proving and disproving termination in the years 2004-2007.