Higher Order Termination

Cynthia Kop

Promotor: Prof.dr. J.W. Klop (VUA)
Co-promotor: Dr. F. van Raamsdonk (VUA)
Vrije Universiteit Amsterdam
Date: 13 November, 2012

Summary

Higher-order term rewriting is a collective name for a number of different formalisms. These formalisms can be used as a higher-order logic, or as the underlying framework of functional programming languages. Termination of term rewriting systems is an important research topic, as it is closely connected with correctness.

This thesis studies termination of higher-order term rewriting. In particular, we consider the AFSM formalism, which can be used to analyse various existing formalisms in one go. A recurring theme in these approaches is the use of transformations, which can often be used to bring a termination problem in an easier shape.

Higher-order term rewriting systems are an extension of first-order term rewriting systems. First-order systems are typically easier to analyse, and many termination results already exist. An obvious direction for research is to extend these existing methods to the higher-order setting. In this thesis we study three methods: polynomial interpretations, path orderings and dependency pairs. These are some of the most prominent termination techniques in the first-order world, and moreover they are automatable: there are numerous tools which can automatically prove or disprove termination of a large number of first-order term rewriting systems.

Automation is a crucial aspect of termination research, in the higher-order setting as well as the first-order one. For while it is nice to know that a program will always find a solution, it is much nicer if you don’t have to make a manual effort to show this! For that reason, almost all techniques introduced in this work have been implemented in the termination tool WANDA, available at http://wandahot.sourceforge.net.