On the Design of a Correct Freeness Analysis for Logic Programs

Michael Codish, Dennis Dams, Gilberto Filé and Maurice Bruynooghe

The Journal of Logic Programming; 28 (3): 181-206, 1996

Abstract:

Several proposals for computing freeness information for logic programs have been put forward in recent literature. The availability of such information has proven useful in a variety of applications, including parallelization of Prolog programs, optimizations in Prolog compilers, as well as for improving the precision of other analyses. While these proposals have illustrated the importance of such analyses, they lack formal justification. Moreover, several have been found incorrect. This paper introduces a novel domain of abstract equation systems describing possible sharing and definite freeness of terms in a system of equations. A simple and intuitive abstract unification algorithm is presented, providing the core of a correct and precise sharing and freeness analysis for logic programs. Our contribution is not only a correct algorithm, but perhaps primarily, the application of a systematic approach in which it is derived by mimicking each step in a suitable concrete unification algorithm. Consequently, the abstract algorithm is intuitive --- as it resembles the concrete algorithm. It is amenable to formal justification --- as the proof of correctness boils down to showing that each step in the concrete algorithm is mimicked by a corresponding step in the abstract algorithm. Finally, it is precise --- as each step mimics only those situations which can arise in the concrete algorithm.

Available: bibtex entry

Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il