Derivationskomplexitätsanalyse

Termersetzung ist ein konzeptionell einfaches, aber mächtiges abstraktes Berechenbarkeitsmodell, welches großen Teilen der deklarativen Programmierung zugrunde liegt. In diesem Projekt interessieren wir uns für das - im Allgemeinen unentscheidbare - Terminationsproblem in der Termersetzung, sowie für die Komplexität von Ersetzungssystemen, die anhand der maximalen Länge von Ableitungsschritten, also Ersetzungsschritten gemessen wird. Im Bereich der Termersetzung wurden mächtige Methoden entwickelt, um die Termination eines gegebenen Ersetzungssystems nachzuweisen. Frühere Forschung hat sich dabei besonders auf die Entwicklung geeigneter Reduktionsordnungen konzentriert, mit denen die Termination direkt nachgewiesen werden kann. In den letzten Jahren hat sich die Ausrichtung eher auf Transformationstechniken wie die Dependency Pair Methode oder Semantic Labelling verschoben. Diese Techniken können benutzt werden, um die Termination eines gegebenen Ersetzungssystems automatisch zu beweisen. Moderne Terminationsbeweiser können Termination und sogar Nichttermination in wenigen Sekunden feststellen. Allerdings ist das Terminationsverhalten eines Ersetzungssystems nicht die einzige interessante Eigenschaft eines solchen. Eine andere interessante Eigenschaft ist die Komplexität des Ersetzungssystems. Wobei hier als Komplexität die maximale Anzahl der Ersetzungsschritte gemessen wird. Dieser Begriff der Komplexität wird überlicherweise als Derivationskomplexität bezeichnet. Das Ziel dieses Projektes ist es Derivationskomplexitätsanalyse modern zu machen, indem die Derivationskomplexität, die von modernen Terminationstechniken induziert wird, studiert wird. nützlich zu machen, indem Verfeinerungen bestehender Terminationstechniken entwickelt werden, die garantieren, dass die induzierte Derivationskomplexität durch eine Funktion von niedriger Berechenbarkeitskomplexität gebunden ist, etwa durch eine in polynomieller Zeit berechenbare Funktion. ausdrucksstark zu machen, indem die Derivationskomplexität von höherstufigen Ersetzungssystemen, sowie von Ersetzungssystemen, die auf bestimmten Strategien aufbauen untersucht werden. Zusätzlich wollen wir sicherstellen, dass die in diesen drei Teilen erzielten Resultate berechenbare und präzise Schranken liefern. Dadurch stellen wir sicher, dass wir instruktive obere Schranken automatisch produzieren können. Wir werden diese in das Tyrolean Termination Tool, ein Terminationsbeweiser, der von unserer Arbeitsgruppe entwickelt wird, einbauen. Dies wird die Ausdrucksfähigkeit des Tyrolean Termination Tools weiter erhöhen, da der Benutzer nicht nur Information über das Terminationsverhalten des analysierten Ersetzungssystems erhält, sondern auch Informationen zur Derivationskomplexität.

Term rewriting is a conceptual simple, but powerful abstract model of computation that underlies much of declarative programming. In this project proposal we are interested in the - general undecidable - termination problem in term rewriting and the complexity of rewrite systems measured by the maximal length of derivations, i.e., rewrite steps. In the area of term rewriting powerful methods have been introduced to establish termination of a given term rewrite system. Earlier research mainly concentrated on inventing suitable reduction orders capable of proving termination directly. In recent years the emphasis shifted towards transformation techniques like the dependency pair method or semantic labelling. These techniques can be used to prove termination of a given rewrite system automatically. Modern termination provers can often establish termination or nontermination of the input rewrite system in a couple of seconds. However, termination of a rewrite system is only one property of a rewrite system of interest. Another interesting property is the complexity of the term rewriting system. Here complexity is measured as the maximal length of derivations. This notion of complexity is usually called derivational complexity in the literature. The goal of this project is to make derivational complexity analysis modern by studying the derivational complexities induced by modern termination techniques, useful by establishing refinements of existing termination techniques guaranteeing that the induced derivational complexity is bounded by a function of low computational complexity, for example a polytime computable function, broad by analysing the derivational complexities of higher-order rewrite systems and for rewrite systems based on particular rewrite strategies. Further we want to ensure that the results that we will develop in these three parts provide computable and precise bounds. Thus guaranteeing that we can establish instructive upper bounds automatically. We will incorporate them into the Tyrolean Termination Tool, a termination prover which is developed in our research group. This will make the Tyrolean Termination Tool more expressive by rendering the user not only information about the termination behaviour of the analysed term rewrite system, but also about its derivational complexity.