The limits of fixed-order computation (Q5940930): Difference between revisions

Fixed-order computation rules, used by Prolog and most deductive database systems, do not suffice to compute the well-founded semantics [\textit{A. Van Gelder, K. A. Ross} and \textit{J. S. Schlipf}, J. ACM 38, No. 3, 620-650 (1991; Zbl 0799.68045)] because they cannot properly resolve loops through negation. This inadequacy is reflected both in formulations of SLS-resolution [(*) \textit{T. C. Przymusinski}, in: Proc. 8th ACM SIGACT-SIGMOD-SIGART Symp. on Principles of Database Systems, ACM Press, Philadelphia, Pennsylvania, March 1989, pp. 11-21; \textit{K. A. Ross}, J. Log. Program. 13, No 1, 1-22 (1992; Zbl 0773.68064)] which is an ideal search strategy, and in more practical strategies like SLG [\textit{W. Chen} and \textit{D. S. Warren}, J. ACM 43, No. 1, 20-74 (1996; Zbl 0882.68050)] or Well-Founded Ordered Search [\textit{P. J. Stucky} and \textit{S. Sudarshan}, J. Log. Program. 32, No. 3, 171-206 (1977)]. Typically, these practical strategies combine an inexpensive fixed-order search with a relatively expensive dynamic search, such as an alternating fixed point [\textit{A. Van Gelder}, J. Comput. Syst. Sci. 47, No. 1, 185-221 (1993; Zbl 0793.68039)]. 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 [\textit{K. A. Ross}, J. ACM 41, No. 6, 1216-1266 (1994; Zbl 0830.68028)], 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 (*) 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.