Proving termination of rewriting with the dependency pair framework

Abstract

Termination ist neben Konfluenz die wichtigste und grundlegendste Eigenschaft von Termersetzungsystemen (TRS).Wenn ein TRS terminiert, ist es garantiert, dass jede Strategie der Verarbeitung mit dem System immer mit einer Normalform beendet. Aber die Unentscheidbarkeit der Termination zeigt, dass es keine automatisierte Methode gibt, die diese Eigenschaft für alle terminierenden TRS beweisen kann. Zahlreiche syntaktische sowie semantische Methoden wurden entwickelt, aber es gibt noch viele wichtige TRS, deren Termination nicht gezeigt werden kann. Das Dependency Pair Framework (eingeführt in [AG00] und allgemein formuliert im [GTS05], kurz DP Framework genannt) ist momentan die am weitesten verbreitete Methode. Es kann die Klasse von Systemen, deren Terminierung automatisch beweisbar ist, signifikant erhöhen. Der Vorteil des Framework liegt in der hohen Flexibilität aufgrund seiner allgemeinen und modularen Struktur, und in der Fähigkeit, andere allgemeine Terminationsbeweis-Methoden zu integrieren. Die vorliegende Arbeit wird das DP Framework und seine Bestandteile zusammenfassen.<br />Zuerst präsentieren wir die theoretischen Grundlagen des Framework, bei dem diverse Dependency Pair Processors (DP processors) anfängliche Terminationsbeweis-Probleme in endlich viele einfachere solche Probleme transformieren. Dann, im Hauptteil der Zusammenfassung, geben wir einen umfassenden Überblick über einige wichtige DP Processor-Typen. DP Processors lassen sich als Terminations-Techniken im DP Framework verstehen. Ein Terminationsbeweis im DP Framework ist im Wesentlichen die wiederholte Anwendung von DP Processors. Für jeden DP Processor erarbeiten wir die grundlegende Ideen und Theorie, präsentieren einige Verfeinerungen, und illustrieren Anwendungen mit Beispielen. Weiterhin erarbeiten wir auch einen Überblick über einige allgemeine Terminationsbeweis- Methoden, z.B. Reduktionsordnungen (Polynominterpretation, Matrixinterpretation, Simplifikationsordnung), Match-Bounds, und Semantic Labeling, die auch im DP Framework angewandt werden können.<br />

Termination is besides confluence the most important and fundamental property of term rewriting systems (TRSs). If a TRS is terminating, then this guarantees that every strategy of computing with the system will always end with normal forms. But unfortunately, the undecidability of termination shows that there cannot be an automated method that will succeed in proving termination of all terminating TRSs.<br />Numerous syntactical as well as semantical methods have been developed, but there are still many important TRSs whose termination cannot be shown. The dependency pair framework (introduced in [AG00] and generally formulated in [GTS05], shortly called the DP framework) is currently the most powerful method that can increase significantly the class of systems where termination is provable automatically. The power of the framework lies in its high flexibility, due to its general and modular structure, and the ability to incorporate other general termination proof methods. This thesis will summarize the DP framework and its ingredients. First, we summarize the theoretical foundations of the framework, that allows various dependency pair processors (DP processors) to successively simplify the initial termination proof problems. Then, as the main part of the summary, we will give a comprehensive survey of some important types of DP processors. The DP processors can be seen as the termination techniques in the DP framework. All termination proofs in the DP framework are basically obtained by repeated applications of DP processors. For each DP processor we work out the basic underlying ideas and theory, present some refinements, and illustrate their applications by examples. In addition, we will also include a short survey of some general termination proof methods, e.g. reduction orders (polynomial interpretations, matrix interpretations, simplification orders), match-bounds, and semantic labeling, which can also be applied within the DP framework.<br />