The limits of fixed-order computation

Fixed-order computation miles, used by Prolog and most deductive database systems, do not suffice to compute the well-founded semantics [19] because they cannot properly resolve loops through negation. This inadequacy is reflected both in formulations of SLS-resolution [8, 12] which is an ideal search strategy, and in more practical strategies like SLG [3], or Well-Founded Ordered Search [16]. Typically, these practical strategies combine an inexpensive fixed-order search with a relatively expensive dynamic search, such as an alternating fixpoint [18]. 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 [13], 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 [8] to formulate the class of left-toright dynamically stratified programs. We show that this class properly includes other classes of fixed-order stratified programs. Furthermore, we introduce SLGot,at, a variant of SLG resolution that uses a fixed-order computation rule, and prove that it correctly evaluates ground left-toright dynamically stratified programs. We outline how SLG,tr~t 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.