Derivation of linear size relations by abstract interpretation

Abstract

We propose an automated method for deriving linear size relations. Linear size relations are linear relations (the solutions of a system of linear equations) over the natural numbers. We associate one such relation to each predicate occurring in a given pure definite logic program. The linear size relation is a linear overestimation of the relation that exists between the sizes (with respect to some given norm) of the arguments of atoms in the least Herbrand model for the given predicate. Size relations have been studied before and were often referred to as interargument relations. The main contribution of this paper is that our method for deriving the relations is presented as an application of abstract interpretation. Its abstract domain consists of arnne subspaces or linear varieties, and the basic operations (procedure entry, procedure exit, etc.) are expressed in terms of operations from linear algebra. Applications of the technique are situated in e.g. automatic termination analysis and the specialisation of constraints in a constraint logic language.