On the complexity analysis of static analyses

ABSTRACT

This paper argues that for many algorithms, and static analysis algorithms in particular, bottom-up logic program presentations are clearer and simpler to analyze, for both correctness and complexity, than classical pseudo-code presentations. The main technical contribution consists of two theorems which allow, in many cases, the asymptotic running time of a bottom-up logic program to be determined by inspection. It is well known that a datalog program runs in O(n^k) time where k is the largest number of free variables in any single rule. The theorems given here are significantly more refined. A variety of algorithms are presented and analyzed as examples.

REFERENCES

• 1: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 2: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 3: Alexander Aiken , Edward L. Wimmers , T. K. Lakshman, Soft typing with conditional types, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177847]
• 4: Andrew W. Appel, Modern compiler implementation in Java: basic techniques, Cambridge University Press, New York, NY, 1997
• 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: Bondorf, A., and Jorgensen, A. 1993. Efficient analysis for realistic off-line partial evaluation. J. Funct. Program. 3, 3, 315--346.
• 7: 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]
• 8: 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]
• 9: Dijkstra, E. W. 1959. A note on two problems in connection with graphs. Numer. Math. 1, Oct., 269--271.
• 10: Downing, W., and Gallier, J. W. 1984. Linear time algorithms for testing the satisfiability of propositional horn formulae. J. Logic Program. 1, 3, 267--284.
• 11: Jason Eisner , Giorgio Satta, Efficient parsing for bilexical context-free grammars and head automaton grammars, Proceedings of the 37th annual meeting of the Association for Computational Linguistics on Computational Linguistics, p.457-464, June 20-26, 1999, College Park, Maryland [doi>10.3115/1034678.1034748]
• 12: Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su , Alexander Aiken, Partial online cycle elimination in inclusion constraint graphs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.85-96, June 17-19, 1998, Montreal, Quebec, Canada
• 13: Nevin Heintze, Set-based analysis of ML programs, Proceedings of the 1994 ACM conference on LISP and functional programming, p.306-317, June 27-29, 1994, Orlando, Florida, United States
• 14: Heintze, N., and Jaffar, J. 1990a. A decision procedure for a class of set constraints. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 42--51.
• 15: 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]
• 16: Nevin Heintze , David McAllester, Linear-time subtransitive control flow analysis, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.261-272, June 16-18, 1997, Las Vegas, Nevada, United States
• 17: Nevin Heintze , David McAllester, On the Cubic Bottleneck in Subtyping and Flow Analysis, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.342, June 29-July 02, 1997
• 18: Fritz Henglein, Breaking through the n3barrier: faster object type, Theory and Practice of Object Systems, v.5 n.1, p.57-72, Jan. 1999 [doi>10.1002/(SICI)1096-9942(199901/03)5:1<57::AID-TAPO5>3.0.CO;2-U]
• 19: Dexter Kozen , Jens Palsberg , Michael I. Schwartzbach, Efficient inference of partial types, Journal of Computer and System Sciences, v.49 n.2, p.306-324, Oct. 1994 [doi>10.1016/S0022-0000(05)80051-0]
• 20: Lari, K., and Young, S. J. 1990. The estimation of stochastic context-free grammars using the inside-outside algorithm. Comput. Speech Lang. 4, 1, 35--56.
• 21: Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982 [doi>10.1145/357162.357169]
• 22: McAllester, D. 1996. Inferring recursive types. Available online at http://www.research.mit.edu/∼dmac.
• 23: David Melski , Thomas Reps, Interconvertbility of set constraints and context-free language reachability, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.74-89, June 12-13, 1997, Amsterdam, The Netherlands
• 24: Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 3, 348--375.
• 25: Naughton, J., and Ramakrishnan, R. 1991. Bottom-up evaluation of logic programs. In Computational Logic, J.-L. Lassez and G. Plotkin, Eds. MIT Press, Cambridge, Mass.
• 26: Jens Palsberg, Efficient inference of object types, Information and Computation, v.123 n.2, p.198-209, Dec. 1995 [doi>10.1006/inco.1995.1168]
• 27: Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.4, p.576-599, July 1995 [doi>10.1145/210184.210187]
• 28: Paterson, M. S., and Wegman, M. N. 1978. Linear unification. J. Comput. Syst. Sci. 16, 2 (April), 158--167.
• 29: Fernando C. N. Pereira , David H. D. Warren, Parsing as deduction, Proceedings of the 21st annual meeting on Association for Computational Linguistics, June 15-17, 1983, Cambridge, Massachusetts [doi>10.3115/981311.981338]
• 30: Reps, T. 1994. Demand Interprocedural Program Analysis Using Logic Databases. Kluwer Academic Publishers, Norwell, Mass., pp. 163--196.
• 31: Rocio, V., and Lopes, J. G. 1998. Partial parsing, deduction and tabling. In Proceedings of Tabulation in Parsing and Deduction (TAPD'98) (Paris, France, April 1998), pp. 52--61.
• 32: J Rohmer , R Lescoeur , J M Kerisit, The Alexander method-a technique for the processing of recursive axioms in deductive databases, New Generation Computing, v.4 n.3, p.273-285, 1986 [doi>10.1007/BF03037407]
• 33: Konstantinos Sagonas , Terrance Swift , David S. Warren, XSB as an efficient deductive database engine, Proceedings of the 1994 ACM SIGMOD international conference on Management of data, p.442-453, May 24-27, 1994, Minneapolis, Minnesota, United States
• 34: Shivers, O. 1991. Data flow analysis and type recovery in scheme. In Topics in Advanced Language Implementation, P. Lee, Ed. MIT Press, Cambridge, Mass.
• 35: Robert E. Shostak, An algorithm for reasoning about equality, Communications of the ACM, v.21 n.7, p.583-585, July 1978 [doi>10.1145/359545.359570]
• 36: Shieber, S. M., Schabes, Y., and Pereira, F. 1995. Principles and implementation of deductive parsing. J. Logic Program. 24, 1-2 (July/Aug.), 3--36.
• 37: Hisao Tamaki , Taisuke Sato, OLD resolution with tabulation, Proceedings on Third international conference on logic programming, p.84-98, September 1986, London, United Kingdom
• 38: J. D. Ullman, Bottom-up beats top-down for datalog, Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.140-149, March 1989, Philadelphia, Pennsylvania, United States [doi>10.1145/73721.73736]
• 39: Ullman, J., and Ramakrishnan, R. 1995. A survey of research in deductive database systems. J. Logic Program. 23, 2, 125--150.
• 40: Moshe Y. Vardi, The complexity of relational query languages (Extended Abstract), Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.137-146, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802186]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.6 Logic Programming

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.0 General

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.0 General
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms

General Terms:
Algorithms, Languages, Theory

Keywords:
Algorithms, complexity analysis, logic programming, models of computation, program analysis, programming languages