Establishing that all computations terminate is a fundamental, though generally undecidable, property of computer programs. Therefore, termination analyses that approximate this property have been developed for different programming languages.

This paper focuses on the definition of a termination analysis for logic programs (roughly speaking, simple Prolog programs). In this context, termination analyses proceed by first identifying the program loops and then by looking for a ranking function that maps every call to a well-founded domain so that its value decreases every time a loop is executed. The so-called global approach considers a single ranking function for all loops, while the more flexible local approach allows the use of different ranking functions. In the context of logic programs, ranking functions are often based on the notion of “norm,” a mapping used to measure the size of the arguments of a call.

In this context, the authors show that by providing type declarations (which is not usually required in Prolog implementations), a collection of simple, type-based norms can be automatically inferred. Intuitively speaking, a type-based norm counts the number of subterms in a term of the given type. Then, the authors show that using the combination of different type-based norms as a basis for the definition of ranking functions (following the local approach) results in a more precise termination analysis than existing analyses.

The paper is well written, includes a good introduction to its main subject, and contains many examples that illustrate the technical developments. It also includes formal proofs of correctness and provides a summary of results from a complete experimental evaluation. The results are not surprising, but show that the new approach is actually useful in practice.