Bottom-Up Abstract Interpretation of Logic Programs

摘要

The paper presents a formal framework for the bottom-up abstract interpretationof logic programs which can be applied to approximate answer substitutions, partial answer substitutions and call patterns for a given program and arbitrary initial goal. The framework is based on a T sub P like semantics defined over a Herbrand universe with variables which has previously been shown to determine the answer substitutions for arbitrary initial goals. The first part of the paper reconstructs this semantics to provide a more adequate basis for abstract interpretation. A notion of abstract substitution is introduced and shown to determine an abstract semantic function which for a given program can be applied to approximate the answer substitutions for an arbitrary initial goal. The second part of the paper extends the bottom-up approach to provide approximations of both partial answer substitutions and call patterns. This is achieved by applying Magic Sets and other existing techniques to transform a program in such a way that the answer substitutions of the transformed program correspond to the partial answer substitutions and call patterns of the original program.