You are here

Termination and Complexity

Abstract

Lecturer: Johannes Waldmann, HTWK Leipzig
(http://www.imn.htwk-leipzig.de/~waldmann/)

A computation is terminating if it consists, for each input, of a finite number of steps. The complexity of a computation is this number, as a function of the size of the input.

For the term rewriting model of computation, we will look at these methods for proving termination, and deriving complexity bounds from termination proofs:
       1. Matrix interpretations, and bounding their growth
       2. Relative Termination and modular proofs of termination
       3. Exotic matrix semirings and matchbounds

This is an advanced course. As prerequisite, students should have a working knowledge of basics of rewriting and termination (e.g., as in Chapter 5 of Baader/Nipkow: Term Rewriting and All That).

Slides for the presentations can be accessed here.