Termination analysis is a fundamental part of program verification, and is also used extensively in theorem proving. Automatic termination analysis seeks to verify termination of a program (without user assistance, or with minimal assistance).

The size-change termination principle is a powerful criterion for deciding termination of pure first-order functional programs. More information on size-change termination can be found here (page by Chin Soon Lee).

Higher-Order Programs

We have been extending the size-change termination analysis to higher-order purely functional languages, building on Neil Jones's work on termination analysis of the lambda-calculus. This handles programs written in the purely functional subset of OCaml, though other languages like Scheme could be handled without too much trouble. Lazy languages like Haskell can also be handled, by translating lazy programs into strict ones.

Challenges

What's difficult about it?

• Control- and Data-flow analysis of higher-order programs is rather tricky...

  This is the current focus of my work. The starting point is the idea of a k-CFA of a program, due to Olin Shivers, but in many cases this is insufficient (in particular, termination analysis of lazy programs is difficult). We are investigating other techniques to approximate the environments that can occur in a computation, in particular the use of tree automata.

• Finding "higher-order" termination

  The SCT principle proves termination by showing that along every self-call in the program, some (well-founded) parameter decreases. For example, the map function:

         map f xs = if null xs then [] else f (head xs) :: (tail xs)
  

  terminates because the xs parameter becomes smaller at each recursive call. To prove termination of more interesting higher-order programs, it is necessary to extend the notion of size to higher-order values as well.

Resources

A tech report on the subject is available. There is also an experimental implementation in OCaml, with some rough edges.

Contact

Damien Sereni