Deja Vu in Fixpoints of Logic Programs

Abstract

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 needs not be re-used in subsequent interations, 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.