Abstract

This thesis is concerned with termination and complexity analysis of term rewrite systems. Term rewriting is a formal model of computation based on equational logic. Due to Turing-completeness, all interesting properties of term rewrite systems are undecidable. Nevertheless, many powerful termination techniques have been developed in the course of time. In this thesis, we focus on polynomial interpretations and matrix interpretations, giving the answer to a number of open research questions related to termination and complexity analysis.

The method of polynomial interpretations is one of the oldest termination techniques, but still successfully employed in many automatic termination analyzers. One distinguishes three variants, polynomial interpretations with real, rational and integer coefficients, which raises the question of their mutual relationship with regard to termination proving power. In 2006, a partial answer was given by Lucas who managed to prove that there are term rewrite systems that can be shown terminating by polynomial interpretations with rational coefficients, but cannot be shown terminating using integer polynomials only. He also proved the
existence of systems that can only be handled by polynomial interpretations with real (algebraic) coefficients. In this thesis, we extend these results and give the full picture of the relationship, thereby refuting a common yet unproven belief in the term rewriting community about this relationship.

Since their inception in 2006, matrix interpretations have evolved into one of the most important termination techniques. In analogy to polynomial interpretations, there are three variants depending on the domain of the matrix entries, matrix interpretations over the real, rational and natural numbers. We clarify their relationship by showing that matrix interpretations over the reals are more powerful than matrix interpretations over the rationals, which are in turn more powerful than matrix interpretations over the natural numbers. We also show how the choice of the matrix dimension affects termination proving power. Beyond termination analysis, matrix interpretations are the most important technique for obtaining polynomial upper bounds on the (derivational) complexity of term rewrite systems, where the aim is to obtain information about the maximal length of rewrite sequences in relation to the size of their initial term. In particular, triangular matrix interpretations over the natural numbers are known to induce polynomial upper bounds. Recently, this method was improved by an automata-based approach giving a complete characterization of polynomially bounded matrix interpretations over the natural numbers. In this thesis, we present an algebraic approach which subsumes all previous approaches and provides a complete characterization of polynomially bounded matrix interpretations over the real, rational and natural numbers.

BibTeX

@phdthesis{FN12,
  author    = "Friedrich Neurauter",
  title     = "Termination Analysis of Term Rewriting by Polynomial
               Interpretations and Matrix Interpretations",
  school    = "University of Innsbruck",
  year      = 2012
}