3rd International School on Rewriting

21 – 26 July 2008, Obergurgl, Austria

Program – Track B – Advanced Topics in Termination

Lecturer

Dieter Hofbauer

Introduction

After a survey of basic termination criteria and transformation techniques as used in current termination provers, we put the main emphasis on two topics: proof techniques based on automata theory, and derivational complexity.

Finite automata on strings or trees occur in the analysis of match-bounded rewriting systems. These systems are terminating, and in the case of string rewriting they preserve regularity of languages, which results in the decidability of certain strong termination and normalization properties. As another application of formal language theory, we relate matrix interpretations to weighted automata over appropriate semi-rings. Two alternatives for synthesizing matrix interpretations are presented: SAT solving and backward completion of weighted automata.

Derivational complexity relates the length of derivations to the size of starting terms. We review results on upper and lower complexity bounds induced by termination proofs via interpretations or via syntactically defined path orders, and by relative termination proofs. In some cases, these observations can be extended to characterizations of complexity classes, for instance of the class of functions computable in polynomial time. Finally, various approaches towards an automated complexity analysis are discussed.

Material

• slides
• exercises