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 [\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.
- On some computational orders of convergence
- scientific article; zbMATH DE number 6426780
- Limits of computation. From a programming perspective
- Complexity of fixed point computation
- Computational complexity of fixed points
- scientific article; zbMATH DE number 2085171
- Computability of Fraïssé limits
- Third-Order Computation and Bounded Arithmetic
- scientific article; zbMATH DE number 1344922
- scientific article; zbMATH DE number 784042
- A logic programming system for nonmonotonic reasoning
- A procedural semantics for well-founded negation in logic programs
- An extension of Van Gelder's alternating fixpoint to magic programs
- Efficient access mechanisms for tabled logic programs
- HiLog: A foundation for higher-order logic programming
- scientific article; zbMATH DE number 3872640 (Why is no real title available?)
- scientific article; zbMATH DE number 4199656 (Why is no real title available?)
- scientific article; zbMATH DE number 4147555 (Why is no real title available?)
- scientific article; zbMATH DE number 1332641 (Why is no real title available?)
- Modular stratification and magic sets for Datalog programs with negation
- Negation by default and unstratifiable logic programs
- Tabled evaluation with delaying for general logic programs
- Tabulated resolution for the well-founded semantics
- The alternating fixpoint of logic programs with negation
- The well-founded semantics for general logic programs
- Well-founded ordered search: Goal-directed bottom-up evaluation of well-founded models
- On the limits of computations with the floor function
- XSB: extending Prolog with tabled logic programming
- From heaps of matches to the limits of computability
- Well-founded ordered search: Goal-directed bottom-up evaluation of well-founded models
- An abstract machine for fixed-order dynamically stratified programs
- Logic Programming and Nonmonotonic Reasoning
- Static filtering on stratified programs
This page was built for publication: The limits of fixed-order computation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5940930)
