The DP framework for proving termination of term rewriting
type: CreativeWork
description: 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 technique…
abstract: 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 technique…
author: Thiemann, René
language: eng
keywords: info:eu-repo/classification/ddc/004, Terminierung <Informatik>, Termersetzungssystem, Verifikation, Informatik, termination, term rewriting, verification, dependency pairs
date published: 2007
date modified: 2026-07-30T19:43:28Z
provider: RWTH Aachen University
publisher: Networked Digital Library of Theses and Dissertations
type: WebPage
source organization: Publikationsserver der RWTH Aachen University