Deriving constraints among argument sizes in logic programs

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 R n. 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. For any atomic formula (atom, for short) in a rule, we show how to express the vector of its argument sizes as a system of linear equations and inequalities involving sizes of the logical variables that occur in it. This system denes a polycone, which represents the set of feasible argument size vectors. Transformations combine polycones for all atoms in one rule to give the feasible polycone for the entire rule. We introduce a generalized Tucker representation for systems of linear equations. 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 de ne 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 nding a polycone that is a xpoint of a transfor-mation that is derived from both the recursive and nonrecursive rules. Some methods for nding a xpoint are presented, but there are many unresolved problems in this area