 |
Bottom-Up Abstract Interpretation of Logic Programs
Michael Codish, Dennis Dams and Eyal Yardeni
Journal of Theoretical Computer Science;
124 : 93--125,
1994
Abstract:
This paper presents a formal framework for the bottom-up abstract interpretation of 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_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. This facilitates the analysis of concurrent logic programs (ignoring synchronization) and provides a collecting semantics which characterizes both success and call patterns.Available: bibtex entry compressed postscript
Related sites: Abstract from the publisher
Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il