Approximating the success set
of logic programs using
constrained regular types
Lee Naish
A key component of many logic programming analysis tasks is defining a
safe (superset) approximation to the success set of the program.
Our primary application is a declarative mode system which can express
polymorphic modes and linearity information. Others include
analysis of type and groundness dependencies. Even analysis of
procedural properties generally uses declarative information. For
example, termination analyses use inter-argument relations, which can be
seen as safe approximations to the success set. In this paper we show
how the success set can be approximated by \emph{constrained regular
types}. This is a domain similar to regular types but can contain
constraints to express relationships between multisets of
subterms and between well-typedness of subterms. It allows very
precise analysis. Even meta interpreters can be analysed with no loss
of precision. We define constrained regular types and describe a system
which checks if a constrained regular type
is a superset of the success set.
Lee