Recursive Modes For Precise Analysis Of Logic Programs

We present a method to improve the precision of mode analysis of logic programs. The idea is to refine the approximation of non-variable terms into a lattice of recursive modes so the recursive data types having proper but not ground instantiation states can be analyzed more precisely. This refinement is significant since the incomplete data structures are a useful technique in logic programming, but the analysis for its applications is usually inaccurate without using the much more expensive domains like type graphs. Because the modes are important to many other analyses, the improvements in the precision can have significant overall benefits. In particular, this idea can improve the precision of analysis for reference-chain patterns and the generalized type synthesis. Perhaps more interesting is that it suggests a method to describe and reason about the modes more precisely without depending on the notion of types. In this paper, we shall demonstrate how to develop a simple abstract domain of recursive modes as an application of the Galois connection approach to abstract interpretation. To evaluate the benefits, a generic analyzer has been designed and implemented.