Abstract

This thesis is concerned with derivational complexity analysis of term rewrite systems. Term rewriting is a simple, but Turing-complete model of computation which resembles first-order functional programming. Derivational complexity is a natural measure of time complexity for term rewrite systems: it relates the maximum number of computational steps in term rewriting (rewrite steps) with the size of the initial term. In the literature, there exist many results certifying upper bounds on the derivational complexity of a term rewrite system whose termination can be proved by certain techniques. In this thesis, we expand upon these results by the following contributions.

First, we determine the hardness of deciding whether a certain class of functions is an upper bound on the derivational complexity of a given term rewrite system. For that, we employ the arithmetical hierarchy, a device for classifying the degree of undecidability of decision problems. Although term rewriting has some significant differences from other models of computation, it turns out that the hardness of this decision problem is the same as for the corresponding decision problem for Turing Machines.

Second, we consider variants of existing termination proof techniques which have been defined specifically for derivational complexity analysis: context dependent interpretations and restrictions of matrix interpretations. We state complexity results corresponding to these techniques. Moreover, despite their seeming difference, we present an equivalence between important subsets of them.

Third, we consider the currently most important technique for proving termination of term rewrite systems: the dependency pair framework. It is a framework for combining many small partial proof arguments (which are formalised as DP processors) into a complete termination proof of the
considered term rewrite system. Moreover, the possibility to define new DP processors makes the dependency pair framework easily extensible. While, as
stated before, complexity results exist for many (direct) termination proof techniques, no results existed for any DP processors in the dependency pair framework before. We consider the most important DP processors and give derivational complexity bounds term rewrite systems whose termination can be proved by various combinations of these DP processors. Moreover, we provide examples which show that all these complexity bounds are essentially optimal.

Finally, we give a brief overview over the software tool TCT, which is an automatic prover for upper complexity bounds for term rewrite systems. The focus of TCT is polynomial bounds. In particular, those techniques mentioned in this thesis, from which a polynomial upper bound on the derivational complexity of the considered term rewrite system can be concluded, have been implemented in TCT.

BibTeX

@phdthesis{AS12,
  author    = "Andreas Schnabl".
  title     = "Derivational Complexity Analysis Revisited",
  school    = "University of Innsbruck",
  year      = 2012
}