The DP framework for proving termination of term rewriting

Thiemann, René; Giesl, Jürgen

doi:28196

The DP framework for proving termination of term rewriting = Das DP Rahmenwerk zum Termierungsbeweis von Termersetzungssystemen

Thiemann, René (Author)

2007

Verantwortlichkeitsangabevorgelegt von René Thiemann

ImpressumAachen : Publikationsserver der RWTH Aachen University 2007

UmfangII, 211 S. : graph. Darst.

ReiheAachener Informatik-Berichte ; 2007,17

Aachen, Techn. Hochsch., Diss., 2007

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Giesl, Jürgen (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2007-10-24

Online
URN: urn:nbn:de:hbz:82-opus-20666
URL: https://publications.rwth-aachen.de/record/62510/files/Thiemann_Rene.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Terminierung <Informatik> (Genormte SW) ; Termersetzungssystem (Genormte SW) ; Verifikation (Genormte SW) ; Informatik (frei) ; termination (frei) ; term rewriting (frei) ; verification (frei) ; dependency pairs (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Terminierung ist die fundamentale Eigenschaft eines Programms, dass für jede Eingabe die Auswertung schließlich beendet wird und eine Ausgabe geliefert wird. Obwohl die Frage, ob ein gegebenes Programm terminiert, unentscheidbar ist, wurden viele Techniken entwickelt, um die Frage der Terminierung für viele Programme automatisch zu beantworten. Terminierung von Termersetzungssystemen ist ein besonders interessantes und weit erforschtes Gebiet: Da der Basis-Auswertungsmechanismus vieler Programmiersprachen Termersetzung ist, kann man die Terminierungstechniken der Termersetzung erfolgreich einsetzen, um die Terminierung von Programmen automatisch zu analysieren. Trotzdem gibt es noch viele Programme, die mit den momentan verfügbaren und automatisierbaren Techniken nicht bewältigt werden können. In dieser Arbeit erweitern wir bestehende Techniken und entwickeln neue Methoden zur automatischen Terminierungsanalyse von Termersetzungssystemen. Eine der momentan mächtigsten Methoden ist der Dependency-Pair Ansatz. Bisher wurde dieser Ansatz als eine von vielen möglichen Methoden zum Terminierungsbeweis gesehen. Wir zeigen, dass Dependency-Pairs auch als ein generelles Konzept genutzt werden können, um beliebige Terminierungstechniken zu integrieren. Auf diesem Weg können die Vorteile aller Techniken kombiniert werden, und ihre Modularität und Mächtigkeit werden somit bedeutend vergrößert. Wir bezeichnen dieses neue Konzept als das „Dependency-Pair Rahmenwerk", um es vom bisherigen „Dependency-Pair Ansatz" zu unterscheiden. Dieses Rahmenwerk erleichtert auch die Entwicklung neuer Methoden zur Terminierungsanalyse. Um dies zu demonstrieren, entwickeln wir viele neue Techniken im Dependency-Pair Rahmenwerk. Sie können erfolgreich auf Programme angewendet werden, deren Terminierungsnachweis zuvor eine Herausforderung darstellte. So werden zum Beispiel neue Wege beschrieben, wie man Programme behandelt, die Akkumulatoren verwenden, die Programmkonstrukte höherer Ordnung enthalten, oder die nur terminieren, weil eine gewisse Auswertungsstrategie zugrunde liegt. Zudem zeigen wir, wie man Terminierung widerlegen kann, auch wenn eine Auswertungsstrategie vorgegeben ist. Alle präsentierten Techniken sind auf einheitliche Weise formuliert und in unserem voll-automatischen Terminierungsbeweiser AProVE implementiert. Die Bedeutung unserer Resultate kann bei der jährlichen nternationalen „Termination Competition" gesehen werden, bei der die führenden automatisierten Beweiser versuchen, die Terminierung von Programmen aus unterschiedlichen Bereichen der Informatik zu analysieren: Ohne die Beiträge dieser Arbeit wäre AProVE nicht der Gewinner in den Jahren 2004 bis 2007.

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.

Fulltext:
PDF