DERIVING LINEAR SIZE RELATIONS FOR LOGIC PROGRAMS BY ABSTRACT INTERPRETATION

We propose an automatic method for deriving linear size relations, whi ch specify, with respect to some given norm, linear relationships betw een the sizes of the arguments of atoms in the least Herbrand model of a definite Horn clause program. The method is presented as an applica tion of abstract interpretation. Its abstract domain consists of affin e subspaces or linear varieties, and operations on elements of the dom ain are expressed in terms of operations from linear algebra. The main application of the technique is situated in automatic termination ana lysis. Others are complexity and granularity analysis and the speciali sation of constraints in constraint logic languages.