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.