Analysis of Polymorphically Typed
Logic Programs Using ACI-Unification
Abstract
Analysis of (partial) groundness is an important application of
abstract interpretation. There are several proposals for improving the
precision of such an analysis by exploiting type information,
including
our own work
with Hill and King, where we had shown how
the information present in the type declarations of a program can be
used to characterise the degree of instantiation of a term in a
precise and yet inherently finite way. This approach worked for
polymorphically typed programs as in Gödel or HAL. Here, we recast
this approach following Codish, Lagoon and
Stuckey
(Codish and Lagoon, 2000; Lagoon and Stuckey, 2001). To formalise which properties of
terms we want to characterise, we use labelling functions, which
are functions that extract subterms from a term along certain
paths. An abstract term collects the results of all labelling
functions of a term. For the analysis, programs are executed on
abstract terms instead of the concrete ones, and usual
unification is replaced by unification modulo an equality theory which
includes the well-known ACI-theory. Thus we
generalise
(Codish and Lagoon, 2000; Lagoon and Stuckey, 2001)
w.r.t. the type systems considered and
relate those two works.