A finite presentation theorem for approximating logic programs

ABSTRACT

The notion of Cartesian closure on a set of unifiers has been used to define approximations of the least models of logic programs. Such approximations, often called types, are not known to be recursive. In this paper, we use Cartesian closure to define a similar, but more accurate, approximation. The main result proves that our approximation is not only recursive, but that it can be finitely represented in the form of a cyclic term graph. This explicit representation can be used as a starting point for logic program analyzers.

REFERENCES

• 1: D. Angluin and D.N. Hoover, "Regular Prefix Relations" Mathematical Systems Theory 17, pp 167 191, 1984.
• 2: M. Bruynooghe, "A Practical Framework for the Abstract Interpretation of Logic Programs", revised version of report CW-62, Dept. Comp. Sci., K.U. Leuven, 33 p~ges, October 1987.
• 3: M. Bruynooghe and G. Janssens, "An Instance of Abstract Interpretation integrating Type and Mode Inference", Proceedings 5th Int. Conf. on Logic Pro#ramming, K.A. Bowen and R.A. Kowalski (eds), MIT Press, pp 669- 683, August 1988.
• 4: N.C. Heintze and J. Jaffar, "A Finite Presentation Theorem for Approximating Logic Programs", forthcoming CMU and IBM Research Report, 56 pages, October 1989.
• 5: N.C. Heintze and J. Jaffar, "A Decision Procedure for a Class of Herbrand Set Constraints" forthcoming CMU and IBM Research l~port, 4() pages, October 1989.
• 6: Steven S. Muchnick , Neil D. Jones, Program Flow Analysis: Theory and Application, Prentice Hall Professional Technical Reference, 1981
• 7: Neil D. Jones , Steven S. Muchnick, Flow analysis and optimization of LISP-like structures, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.244-256, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567776]
• 8: P. Mishra, "Toward a Theory of Types in PRO- LOG", Proceedings I't IEEE Symposium on Logic Programming, Atlantic City, pp 289- 298, 1984.
• 9: Prateek Mishra , Uday S. Reddy, Declaration-free type checking, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.7-21, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318603]
• 10: M.O. Rabin, "Decidability of Second-order Theories and Automata on Infinite Trees", Transactions of the American Math. Society 141, pp 1 - 35, 1969.
• 11: J.C. Reynolds, "Automatic Computation of Data Set Definitions", Information Processing 68, North-Holland, pp 456 - 461, 1969.
• 12: E. Yardeni , E. Shapiro, A type system for logic programs, Concurrent Prolog: collected papers, MIT Press, Cambridge, MA, 1988

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Theory