The limits of fixed-order computation

Fixed-order computation rules, used by Prolog and most deductive database systems, do not suffice to compute the well-founded semantics (Van Gelder et al., J. ACM 38(3) (1991) 620-650) because they cannot properly resolve loops through negation. This inadequacy is reflected both in formulations of SLS-resolution (Przymusinski, in: Proc. 8th ACM SIGACT-SIGMOD-SIGART Symp. on Principles of Database Systems, ACM Press, Philadelphia, Pennsylvania, March 1989, pp. 11-21; Ross, J. Logic Programming 13(1) (1992) 1-22) which is an ideal search strategy, and in more practical strategies like SLG (Chen and Warren, J. ACM 43(1) (1996) 20-74), or Well-Founded Ordered Search (Stucky and Sudarshan, J. Logic Programming 32(3) (1997) 171-206). Typically, these practical strategies combine an inexpensive fixed-order search with a relatively expensive dynamic search, such as an alternating fixed point (Van Gelder, J. Comput. System Sci. 47(1) (1993) 185-221). 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 (Ross, J. ACM 41(6) (1994) 1216-1266), 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. The class of modularly stratified programs, however, is not closed under simple program transformations such as the HiLog transformation. We address the limits of fixed-order computation by adapting results of Przymusinski (1992) to formulate the class of left-to-right dynamically stratified programs, and show that this class properly includes other classes of fixed-order stratified programs. We then 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. Finally, we indicate how SLG_strat can be used as a basis for computing the well-founded semantics through a search strategy called SLG_RD, for SLG with Reduced use of Delaying.