The Limits of Fixed-Order Computations

Click on the title to obtain a gzip-ed PostScript version of the paper (76K).

Abstract:

Fixed-order computation rules, used by Prolog and most deductive database systems, do not suffice to compute the well-founded semantics because they cannot properly resolve loops through negation. This inadequacy is reflected both in formulations of SLS-resolution which is an ideal search strategy, and in more practical strategies like SLG, or Well-Founded Ordered Search. Typically, these practical strategies combine an inexpensive fixed-order search with a relatively expensive dynamic search, such as an alternating fixpoint. Restricting the search space of evaluation strategies by maximizing the use of fixed-order computation is of prime importance for efficient goal-directed evaluation of the well-founded semantics.

Towards this end, the theory of modular stratification, formulates a subset of normal logic programs whose literals can be statically reordered so that the program can be evaluated using a fixed-order computation rule. However, exploration of larger classes of stratified programs that can be evaluated in this manner has been left open in the literature, perhaps due to the lack of implementation methods that can benefit from such results. We address the limits of fixed-order computation by adapting results of Przymusinski to formulate the class of left-to-right dynamically stratified programs. We show that this class properly includes other classes of fixed-order stratified programs. Furthermore, we introduce SLG-strat, a variant of SLG resolution that uses a fixed-order computation rule, and prove that it correctly evaluates ground left-to-right dynamically stratified programs. We outline how SLG-strat can be used as a basis for restricting the space of possible SLG derivations and, finally, outline how these results are used in the abstract machine of XSB, and can be used in other methods such as Ordered Search of CORAL.