Deja Vu in Fixpoints of Logic Programs
Michael J. Maher, Raghu Ramakrishnan · 1989
We investigate properties of logic programs that permit refinements in their fixpoint evaluation and shed light on the choice of control strategy. A fundamental aspect of a bottom-up computation is that we must constantly check to see if the fixpoint has been reached. If the computation iteratively applies all rules, bottom-up, until the fixpoint is reached, this amounts to checking if any new facts were produced after each iteration. Such a check also enhances efficiency in that duplicate facts need not be re-used in subsequent iterations, if we use the Seminaive fixpoint evaluation strategy. However, the cost of this check is a significant component of the cost of bottom-up fixpoint evaluation, and for many programs the full check is unnecessary. We identify properties of programs that enable us to infer that a much simpler check (namely, whether any fact was produced in the previous iteration) suffices. While it is in general undecidable whether a given program has these properties, we develop techniques to test sufficient conditions, and we illustrate these techniques on some simple programs that have these properties. The significance of our results lies in the significantly larger class of programs for which bottom-up evaluation methods, enhanced with the optimizations that we propose, become competitive with standard (top-down) implementations of logic programs. This increased efficiency is achieved without compromising the completeness of the bottom-up approach; this is in contrast to the incompleteness that accompanies the depth-first search strategy that is central to most top-down implementations.