Termination analysis: some practical properties of the norm and level mapping space

The notions of norm and level mapping play an important role in the context of termination analysis. The goal of this paper to provide some structure on the norm and level mapping space, to analyse that structure and to obtain some new insights in termination analysis. Our motivation for this work is two-fold. First, we aim to obtain a better understanding of the notions of boundedness and rigidity which have been introduced to handle partially instantiated input. In this context we show that whenever a program is acceptable wrt a non-bounded level mapping, there always exists a bounded mapping for which the program is still acceptable. Next, we relate level mappings and norms to their sets of bounded atoms and terms and we take advantage of the order on sets of atoms/terms. We show that this order can be easily expressed in terms of finite sets of argument positions. Maximal sets of bounded atoms (terms) correspond to minimal sets of predicate (functor) argument positions. We use this structure to identify sets of terminating queries for the program and we apply the results in off-line program specialisation to automatically generate termination tests.