From datalog rules to efficient programs with time and space guarantees

ABSTRACT

This paper describes a method for transforming any given set of Datalog rules into an efficient specialized implementation with guaranteed worst-case time and space complexities, and for computing the complexities from the rules. The running time is optimal in the sense that only useful combinations of facts that lead to all hypotheses of a rule being simultaneously true are considered, and each such combination is considered exactly once. The associated space usage is optimal in that it is the minimum space needed for such consideration modulo scheduling optimizations that may eliminate some summands in the space usage formula. The transformation is based on a general method for algorithm design that exploits fixed-point computation, incremental maintenance of invariants, and combinations of indexed and linked data structures. We apply the method to a number of analysis problems, some with improved algorithm complexities and all with greatly improved algorithm understanding and greatly simplified complexity analysis.

REFERENCES

• 1: Serge Abiteboul, Querying Semi-Structured Data, Proceedings of the 6th International Conference on Database Theory, p.1-18, January 08-10, 1997
• 2: Serge Abiteboul , Richard Hull , Victor Vianu, Foundations of Databases: The Logical Level, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 3: Serge Abiteboul , Victor Vianu, Regular path queries with constraints, Proceedings of the sixteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.122-133, May 11-15, 1997, Tucson, Arizona, United States [doi>10.1145/263661.263676]
• 4: Alfred V. Aho , John E. Hopcroft , Jeffrey Ullman , J. D. Ullman , J. E. Hopcroft, Data Structures and Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
• 5: Alexander Aiken, Introduction to set constraint-based program analysis, Science of Computer Programming, v.35 n.2-3, p.79-111, Nov.1.1999 [doi>10.1016/S0167-6423(99)00007-6]
• 6: Francois Bancilhon , David Maier , Yehoshua Sagiv , Jeffrey D Ullman, Magic sets and other strange ways to implement logic programs (extended abstract), Proceedings of the fifth ACM SIGACT-SIGMOD symposium on Principles of database systems, p.1-15, March 24-26, 1986, Cambridge, Massachusetts, United States [doi>10.1145/6012.15399]
• 7: J. Cai, P. Facon, F. Henglein, R. Paige, and E. Schonberg. Type analysis and data structure selection. In B. Moller, editor, Constructing Programs from Specifications, pages 126--164. North-Holland, Amsterdam, 1991.
• 8: J. Cai , R. Paige, Program derivation by fixed point computation, Science of Computer Programming, v.11 n.3, p.197-261, April 1989 [doi>10.1016/0167-6423(88)90033-0]
• 9: Answering Regular Path Queries Using Views, Proceedings of the 16th International Conference on Data Engineering, p.389, February 28-March 03, 2000
• 10: Stefano Ceri , Georg Gottlob , Letizia Tanca, Logic programming and databases, Springer-Verlag New York, Inc., New York, NY, 1990
• 11: Weidong Chen , David S. Warren, Tabled evaluation with delaying for general logic programs, Journal of the ACM (JACM), v.43 n.1, p.20-74, Jan. 1996 [doi>10.1145/227595.227597]
• 12: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 13: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 14: Oege De Moor , David Lacey , Eric Van Wyk, Universal Regular Path Queries, Higher-Order and Symbolic Computation, v.16 n.1-2, p.15-35, March-June 2003 [doi>10.1023/A:1023063919574]
• 15: Javier Esparza , David Hansel , Peter Rossmanith , Stefan Schwoon, Efficient Algorithms for Model Checking Pushdown Systems, Proceedings of the 12th International Conference on Computer Aided Verification, p.232-247, July 15-19, 2000
• 16: Nevin Heintze , Joxan Jaffar, Set Constraints and Set-Based Analysis, Proceedings of the Second International Workshop on Principles and Practice of Constraint Programming, p.281-298, May 02-04, 1994
• 17: Quanzhong Li , Bongki Moon, Indexing and Querying XML Data for Regular Path Expressions, Proceedings of the 27th International Conference on Very Large Data Bases, p.361-370, September 11-14, 2001
• 18: Yanhong A. Liu, Efficiency by Incrementalization: An Introduction, Higher-Order and Symbolic Computation, v.13 n.4, p.289-313, Dec. 1, 2000 [doi>10.1023/A:1026547031739]
• 19: Yanhong A. Liu , Ning Li , Scott D. Stoller, Solving Regular Tree Grammar Based Constraints, Proceedings of the 8th International Symposium on Static Analysis, p.213-233, July 16-18, 2001
• 20: Yanhong A. Liu , Scott D. Stoller, Program optimization using indexed and recursive data structures, Proceedings of the 2002 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.108-118, January 14-15, 2002, Portland, Oregon
• 21: Yanhong A. Liu , Scott D. Stoller, Dynamic Programming via Static Incrementalization, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.288-305, March 22-28, 1999
• 22: Yanhong A. Liu , Scott D. Stoller , Tim Teitelbaum, Static caching for incremental computation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.3, p.546-585, May 1998 [doi>10.1145/291889.291895]
• 23: Yanhong A. Liu , Scott D. Stoller , Tim Teitelbaum, Strengthening invariants for efficient computation, Science of Computer Programming, v.41 n.2, p.139-172, October 2001 [doi>10.1016/S0167-6423(01)00003-X]
• 24: Yanhong A. Liu , Fuxiang Yu, Solving Regular Path Queries, Proceedings of the 6th International Conference on Mathematics of Program Construction, p.195-208, July 08-10, 2002
• 25: David A. McAllester, On the Complexity Analysis of Static Analyses, Proceedings of the 6th International Symposium on Static Analysis, p.312-329, September 22-24, 1999
• 26: J. F. Naughton and R. Ramakrishnan. Bottom-up evaluation of logic programs. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 640--700. The MIT Press, Cambridge, Mass., 1991.
• 27: Flemming Nielson , Hanne Riis Nielson , Helmut Seidl, Automatic Complexity Analysis, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.243-261, April 08-12, 2002
• 28: R. Paige. Formal Differentiation: A Program Synthesis Technique, volume~6 of Computer Science and Artificial Intelligence. UMI Research Press, Ann Arbor, Michigan, 1981. Revision of Ph.D. dissertation, New York University, 1979.
• 29: R. Paige. Programming with invariants. IEEE Software, 3(1):56--69, Jan. 1986.
• 30: R. Paige. Real-time simulation of a set machine on a RAM. In Computing and Information, Vol. II, pages 69--73. Canadian Scholars Press, 1989. Proceedings of ICCI '89: The International Conference on Computing and Information, Toronto, Canada, May 23-27, 1989.
• 31: Robert Paige , Shaye Koenig, Finite Differencing of Computable Expressions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.402-454, July 1982 [doi>10.1145/357172.357177]
• 32: R. Sekar , I. V. Ramakrishnan , Andrei Voronkov, Term indexing, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 33: T. Reps. Program analysis via graph reachability. Information and Software Technology, 40(11-12):701--726, Nov. 1998. Special issue on program slicing.
• 34: J. T. Schwartz , R. B. Dewar , E. Schonberg , E. Dubinsky, Programming with sets; an introduction to SETL, Springer-Verlag New York, Inc., New York, NY, 1986
• 35: W. K. Snyder. The SETL2 Programming Language. Technical report 490, Courant Institute of Mathematical Sciences, New York University, Sept. 1990.
• 36: Hisao Tamaki , Taisuke Sato, OLD resolution with tabulation, Proceedings on Third international conference on logic programming, p.84-98, September 1986, London, United Kingdom

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Constraint and logic languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Code generation; Optimization

  E. Data
  E.1 DATA STRUCTURES
      Subjects: Lists, stacks, and queues; Arrays; Records
  E.2 DATA STORAGE REPRESENTATIONS
      Subjects: Linked representations

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures

  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.3 Languages
          Subjects: Query languages
      H.2.4 Systems
          Subjects: Rule-based databases; Query processing

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program transformation

General Terms:
Algorithms, Languages, Performance

Keywords:
complexity analysis, data structure design, datalog, incremental computation, indexed representations, indexing, linked representations, optimization, program transformation, recursion, tabling