11/01/1993 09:00 AM
Computer Science
The question of whether logic programs with function symbols terminate in a top-down (Prolog-like) execution is considered. Automated termination analysis is an essential tool for generating a suitable control in modern deductive database systems, such as LDL and NAIL! We describe a method of identifying a nonnegative linear combination of bound argument sizes, which (if found) strictly decreases in a top-down execution of logic programs. Testing a termination condition is transformed to a feasibility problem of linear inequalities using duality theory of linear programming. For nontrivial termination proofs, we often need to know the relationship among argument sizes of a predicate. We formalize the relationship by a fixpoint of ``recursive transformation\" mimicking immediate consequence operator. Since the transformation sometimes fails to finitely converge, we provide some practical techniques to resolve this problem. We also need to indicate which arguments are bound to ground terms during goal reduction. A method for deriving such binding information is described in the framework of abstract interpretation. Positive propositional formula are used to represent groundness dependency among arguments of a predicate. This methodology can handle nonlinear recursion, mutual recursion, and cases in which no specific argument is certain to decrease. Several programs that could not be shown to terminate by earlier published methods are handled successfully. Notes: Ph.D. Thesis
