School Homepage

Generalising Def and Pos to Type Analysis

Patricia M. Hill
School of Computing
The University of Leeds
Leeds LS2 9JT
England

Fausto Spoto
Dipartimento Scientifico e Tecnologico
Strada Le Grazie
15 Ca' Vignal
37134 Verona
Italy

Abstract:

This paper is concerned with the type analysis of logic programs where, by \emph{type}, we mean a property closed under instantiation. We define a chain of abstractions from Herbrand constraints to logical formulas via the set of their solutions. Every step of the chain is an instance of abstract interpretation. The use of logical formulas for type analysis is a generalisation of the traditional Boolean domains Def and Pos for groundness analysis. In this context, implication is the logical counterpart of the use of linear refinement. While logical formulas can sometime be used for an actual implementation of our domains, in the general case they are infinite objects. Therefore, we apply a final abstraction from possibly infinite logical formulas to (finite) logic programs. Thus, logic programs are themselves used for the type analysis of logic programs. The advantage of our technique with respect to the many frameworks for type analysis present in the literature is that we have developed our domains by using the formal techniques of abstract interpretation and linear refinement. Therefore, their construction is guided by the underlying theory, from which their properties are derived.

Keywords: Abstract interpretation, domain theory, linear refinement, type theory, type analysis, logic programming.