Deriving constraints among argument sizes in logic programs (extended abstract)

ABSTRACT

In a logic program the feasible argument sizes of derivable facts involving an n-ary predicate are viewed as a set of points in the positive orthant of Rn. We investigate a method of deriving constraints on the feasible set in the form of a polyhedral convex set in the positive orthant, which we call a polycone. Faces of this polycone represent inequalities proven to hold among the argument sizes. These inequalities are often useful for selecting an evaluation method that is guaranteed to terminate for a given logic procedure. The methods may be applicable to other languages in which the sizes of data structures can be determined syntactically. We introduce a generalized Tucker representation for systems of linear equations and show how needed operations on polycones are performed in this representation. We prove that every polycone has a unique normal form in this representation, and give an algorithm to produce it. This in turn gives a decision procedure for the question of whether two set of linear equations define the same polycone. When a predicate has several rules, the union of the individual rule's polycones gives the set of feasible argument size vectors for the predicate. Because this set is not necessarily convex, we instead operate with the smallest enclosing polycone, which is the closure of the convex hull of the union. Retaining convexity is one of the key features of our technique. Recursion is handled by finding a polycone that is a fixpoint of a transformation that is derived from both the recursive and nonrecursive rules. Some methods for finding a fixpoint are presented, but there are many unresolved problems in this area.

REFERENCES

• APP*86: Foto Afrati , Christos Papadimitriou , George Papageorgiou , Athena Roussou , Yehoshua Sagiv , Jeffrey D Ullman, Convergence of sideways query evaluation, Proceedings of the fifth ACM SIGACT-SIGMOD symposium on Principles of database systems, p.24-30, March 24-26, 1986, Cambridge, Massachusetts, United States [doi>10.1145/6012.15400]
• ER87: B.C. Eaves and U. G. Rothblum. Elimination of Quanlifiers of Linear Variables and Corresponding Transfer Principles. Technical Report, Operations Research Dept., Stanford University, 1987.
• FRT85: R. M. Freund, R. Roundy, and M. J. Todd. identifying the Set of Always-Active Constraints in a System of Linear Inequalities by a Single Linear Program. Technical Report, Sloan School of Management, MIT, 1985.
• KLTZ83: M. H. Karwan, V. Lofti, J. Telgen, and S. Zionts. Redundancy in Mathematical Programming: A State-of-the-Art Survey. Springer-Verlag, New York, 1983.
• LM89: J.-L. Lassez and K. McAloon. Simplification and elimination of redundant linear arithmetic constraints. In North American Conf. on Logic Programming, 37-51, 1989.
• MUVG86: Katherine Morris , Jeffrey D Ullman , Allen Van Gelder, Design overview of the NAIL] system, Proceedings on Third international conference on logic programming, p.554-568, September 1986, London, United Kingdom
• Nai83: L. Naish. Automatic generation of control for logic programs. Technical Report 83/6, Dept. of Computer Science, University of Melbourne, Melbourne, Australia, 1983.
• Plu88: L. Pliimer. Termination Proofs for Logic Programs. PhD thesis, Dortman University, 1988.
• PS82: Christos H. Papadimitriou , Kenneth Steiglitz, Combinatorial optimization: algorithms and complexity, Prentice-Hall, Inc., Upper Saddle River, NJ, 1982
• Roc70: R.T. Rockafellar. Convex Analysis. Princeton University Press, Princeton, NJ, 1970.
• SU84: Yehoshua Sagiv , Jeffrey D. Ullman, Complexity of a top-down capture rule, Stanford University, Stanford, CA, 1984
• Tel82: J. Telgen. Minimal representation of convex polyhedral sets. Journal of Optimization Theory and Application, 38(1):1-24, 1982.
• Ull85: Jeffrey D. Ullman, Implementation of logical query languages for databases, ACM Transactions on Database Systems (TODS), v.10 n.3, p.289-321, Sept. 1985 [doi>10.1145/3979.3980]
• UVG88: Jeffrey D. Ullman , Allen Van Gelder, Efficient tests for top-down termination of logical rules, Journal of the ACM (JACM), v.35 n.2, p.345-373, April 1988 [doi>10.1145/42282.42285]
• VG86: Allen Van Gelder, A message passing framework for logical query evaluation, Proceedings of the 1986 ACM SIGMOD international conference on Management of data, p.155-165, May 28-30, 1986, Washington, D.C., United States
• VG89: A. Van Gelder. Deriving Constraints Among Argument Sizes in Logic Programs. Technical Report UCSC-CRL-89-41, University of California, Santa Cruz, CA, 1989.
• Wal88: C. Walther. Automated Termination Proofs. PhD thesis, University of Karlsruhe, 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:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.4 Systems
          Subjects: Query processing

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Logic programming
      I.2.8 Problem Solving, Control Methods, and Search
          Subjects: Heuristic methods

General Terms:
Algorithms, Design, Management, Performance, Theory, Verification