Detecting termination using size-change in parameter values

Abstract

We present a method to automatically detect termination in a strict, first order functional language. This is a first step towards an application of the method on Agda (C. Coquand 1996). The method is based on a paper of Neil Jones et al. To any program, seen as a set of equations defining recursive functions, we associate a graph of calls, whose arcs are themselves graphs. These graphs describe for each call the size relations between the formal parameters and the actual parameters. The termination condition can then be stated in terms of these graphs: each infinite path in the graph of calls must contain an infinitely decreasing thread. What is surprising is that this condition can then be ecided by a fully automatic algorithm. The method is quite general, and it is not dependent of auxiliary requirements like for example lexicographically ordered parameters. We have written a small Haskell prototype and tested this method on some examples.