When size does matter - Termination analysis for typed logic programs

Proofs of termination typically proceed by mapping program states to a well founded domain and showing that successive states of the computation are mapped to elements decreasing in size. Automated termination analysers for logic programs achieve this by measuring and comparing the sizes of successive calls to recursive predicates. The size of the call is measured by a level mapping that in turn is based on a norm on the arguments of the call. A norm maps a term to a natural number. The choice of the norm is crucial for the ability to prove termination. For some programs a fairly complex norm is required. The automated selection of an appropriate norm is a missing link in this research domain and is addressed in this paper. Our proposal is to use the type of a predicate to generate a number of simple norms and to try them in turn for proving the termination of the predicate. Given a term of a certain type, we consider a norm for each of its subtypes, a norm that counts the number of subterms of the term that are of the considered subtype.status: publishe