Type inference for datalog and its application to query optimisation

ABSTRACT

Certain variants of object-oriented Datalog can be compiled to Datalog with negation. We seek to apply optimisations akin to virtual method resolution (a well-known technique in compiling Java and other OO languages) to improve efficiency of the resulting Datalog programs. The effectiveness of such optimisations strongly depends on the precision of the underlying type inference algorithm. Previous work on type inference for Datalog has focussed on Cartesian abstractions, where the type of each field is computed separately. Such Cartesian type inference is inherently imprecise in the presence of field equalities. We propose a type system where equalities are tracked, and present a type inference algorithm. The algorithm is proved sound. We also prove that it is optimal for Datalog without negation, in the sense that the inferred type is as tight as possible. Extensive experiments with our type-based optimisations, in a commercial implementation of object-oriented Datalog, confirm the benefits of this non-Cartesian type inference algorithm.

REFERENCES

• 1: Serge Abiteboul , Cassio Souza dos Santos, IQL(2): A Model with Ubiquitous Objects, Proceedings of the Fifth International Workshop on Database Programming Languages, p.10, September 06-08, 1995
• 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 , Georg Lausen , Heinz Uphoff , Emmanuel Waller, Methods and rules, Proceedings of the 1993 ACM SIGMOD international conference on Management of data, p.32-41, May 25-28, 1993, Washington, D.C., United States
• 4: Roland Backhouse, Galois connections and fixed point calculus, Algebraic and coalgebraic methods in the mathematics of program construction, Springer-Verlag New York, Inc., New York, NY, 2002
• 5: 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]
• 6: Sacha Berger, Emmanuel Coquery, Wlodzimierz Drabent, and Artur Wilk. Descriptive typing rules for Xcerpt and their soundness. In François Fages and Sylvain Soliman, editors, Principles and Practice of Semantic Web Reasoning, volume 3703 of LNCS, pages 85--100. Springer, 2005.
• 7: Piero A. Bonatti, On the decidability of containment of recursive datalog queries - preliminary report, Proceedings of the twenty-third ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 14-16, 2004, Paris, France [doi>10.1145/1055558.1055600]
• 8: Maurice Bruynooghe, John P. Gallagher, and Wouter van Humbeeck. Inference of well-typings for logic programs with application to termination analysis. In Chris Hankin and Igor Siveroni, editors, Static Analysis Symposium (SAS '05), volume 3672 of Lecture Notes in Computer Science, pages 35--51. Springer, 2005.
• 9: Diego Calvanese , Giuseppe De Giacomo , Moshe Y. Vardi, Decidable Containment of Recursive Queries, Proceedings of the 9th International Conference on Database Theory, p.330-345, January 08-10, 2003
• 10: Edward P. F. Chan, Containment and minimization of positive conjunctive queries in OODB's, Proceedings of the eleventh ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.202-211, June 02-05, 1992, San Diego, California, United States [doi>10.1145/137097.137869]
• 11: Surajit Chaudhuri, Finding nonrecursive envelopes for Datalog predicate, Proceedings of the twelfth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.135-146, May 25-28, 1993, Washington, D.C., United States [doi>10.1145/153850.153862]
• 12: Surajit Chaudhuri , Phokion G. Kolaitis, Can Datalog be approximated?, Proceedings of the thirteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.86-96, May 24-27, 1994, Minneapolis, Minnesota, United States [doi>10.1145/182591.182602]
• 13: Horatiu Cirstea and Claude Kirchner. Types for web rule languages: a preliminary study. Technical Report IST5067779/Nancy/I3-D2/D/PU/a1, Rewerse: reasoning on the web, 2004.
• 14: Stavros Cosmadakis , Haim Gaifman , Paris Kanellakis , Moshe Vardi, Decidable optimization problems for database logic programs, Proceedings of the twentieth annual ACM symposium on Theory of computing, p.477-490, May 02-04, 1988, Chicago, Illinois, United States [doi>10.1145/62212.62259]
• 15: Patrick Cousot, Types as abstract interpretations, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.316-331, January 15-17, 1997, Paris, France [doi>10.1145/263699.263744]
• 16: 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]
• 17: Evgeny Dantsin , Thomas Eiter , Georg Gottlob , Andrei Voronkov, Complexity and Expressive Power of Logic Programming, Proceedings of the 12th Annual IEEE Conference on Computational Complexity, p.82, June 24-27, 1997
• 18: Anuj Dawar. Types and indiscernibles in finite models. In J. A. Makowsky, editor, Logic Colloquium '95, Lecture Notes in Logic, pages 51--65. Springer, 1995.
• 19: Oege de Moor, Damien Sereni, Mathieu Verbaere, Elnar Hajiyev, Pavel Avgustinov, Torbjörn Ekman, Neil Ongkingco, and Julian Tibble. .QL: Object-oriented queries made easy. In Ralf Lämmel, João Saraiva, and Joost Visser, editors, Generative and Transformational Techniques in Software Engineering, LNCS. Springer, 2007.
• 20: Oege de Moor , Mathieu Verbaere , Elnar Hajiyev , Pavel Avgustinov , Torbjorn Ekman , Neil Ongkingco , Damien Sereni , Julian Tibble, Keynote Address: .QL for Source Code Analysis, Proceedings of the Seventh IEEE International Working Conference on Source Code Analysis and Manipulation, p.3-16, September 30-October 01, 2007 [doi>10.1109/SCAM.2007.13]
• 21: Andrew Dinn , Norman W. Paton , M. Howard Williams , Alvaro A. A. Fernandes , Maria L. Barja, The Implementation of a Deductive Query Language over an OODB, Proceedings of the Fourth International Conference on Deductive and Object-Oriented Databases, p.143-160, December 04-07, 1995
• 22: Thom W. Frühwirth, Ehud Y. Shapiro, Moshe Y. Vardi, and Eyal Yardeni. Logic programs as types for logic programs. In Logic in Computer Science (LICS), pages 300--309. IEEE Computer Society, 1991.
• 23: John P. Gallagher and Kim S. Henriksen. Type analysis and transformation tool. http://wagner.ruc.dk/Tattoo/, 2007.
• 24: John P. Gallagher, Kim S. Henriksen, and Gourinath Banda. Techniques for scaling up analyses based on pre-interpretations. In M. Gabbrielli and G. Gupta, editors, International Conference on Logic Programming (ICLP '05), volume 3668 of LNCS, pages 280--296. Springer, 2005.
• 25: John P. Gallagher , German Puebla, Abstract Interpretation over Non-deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs, Proceedings of the 4th International Symposium on Practical Aspects of Declarative Languages, p.243-261, January 19-20, 2002
• 26: Nevin Heintze , Joxan Jaffar, A finite presentation theorem for approximating logic programs, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.197-209, December 1989, San Francisco, California, United States [doi>10.1145/96709.96729]
• 27: Jakob Henriksson and Jan Maluszyński. Static type-checking of datalog with ontologies. In Hans Jürgen Ohlbach and Sebastian Schaffert, editors, Principles and Practice of Web Reasoning, volume 3208 of LNCS, pages 76--89. Springer, 2004.
• 28: John Hughes, Type Specialisation for the lambda-Calculus; or, A New Paradigm for Partial Evaluation Based on Type Inference, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.183-215, February 12-16, 1996
• 29: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 30: Benjamin S. Lerner , Matthew Flower , Dan Grossman , Craig Chambers, Searching for type-error messages, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 31: Alon Y. Levy , Dan Suciu, Deciding containment for queries with complex objects (extended abstract), Proceedings of the sixteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.20-31, May 11-15, 1997, Tucson, Arizona, United States [doi>10.1145/263661.263665]
• 32: W. Litwin , T. Risch, Main Memory Orientated Optimization of OO Queries Using Typed Datalog with Foreign Predicates, IEEE Transactions on Knowledge and Data Engineering, v.4 n.6, p.517-528, December 1992 [doi>10.1109/69.180603]
• 33: Mengchi Liu , Gillian Dobbie , Tok Wang Ling, A logical foundation for deductive object-oriented databases, ACM Transactions on Database Systems (TODS), v.27 n.1, p.117-151, March 2002 [doi>10.1145/507234.507237]
• 34: Kim Marriott , Harald Søndergaard , Neil D. Jones, Denotational abstract interpretation of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.607-648, May 1994 [doi>10.1145/177492.177650]
• 35: Atsushi Ohori , Peter Buneman , Val Breazu-Tannen, Database programming in Machiavelli—a polymorphic language with static type inference, Proceedings of the 1989 ACM SIGMOD international conference on Management of data, p.46-57, June 1989, Portland, Oregon, United States
• 36: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 37: Semmle Ltd. Company website with free downloads, documentation, and discussion forums. http://semmle.com, 2007.
• 38: Oded Shmueli, Equivalence of datalog queries is undecidable, Journal of Logic Programming, v.15 n.3, p.231-241, Feb. 1993 [doi>10.1016/0743-1066(93)90040-N]
• 39: Vijay Sundaresan , Laurie Hendren , Chrislain Razafimahefa , Raja Vallée-Rai , Patrick Lam , Etienne Gagnon , Charles Godin, Practical virtual method call resolution for Java, ACM SIGPLAN Notices, v.35 n.10, p.264-280, Oct. 2000
• 40: Jeffrey D. Ullman. A comparison between deductive and object-oriented database systems. In 2nd International Conference on Deductive and Object-Oriented Databases, LNCS, pages 263--277, 1991.
• 41: M. Y. Vardi, Invited talk: automata theory for database theoreticians, Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.83-92, March 1989, Philadelphia, Pennsylvania, United States [doi>10.1145/73721.73729]

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.3 Languages
          Subjects: Query languages

General Terms:
Languages, Performance

Keywords:
datalog, query optimization, type inference