This paper focuses on the inference of modes for which a logic program is guaranteed to terminate. This generalises traditional termination analysis where an analyser tries to verify termination for a specified mode. Our contribution is a methodology in which components of traditional termination analysis are combined with backwards analysis to obtain an analyser for termination inference. We identify a condition on the components of the analyser which guarantees that termination inference will infer all modes which can be checked to terminate. The application of this methodology to enhance a traditional termination analyser to perform also termination inference is demonstrated.
This paper draws on results from two areas: termination (checking) analysis and backwards analysis. It shows how to combine components implementing these so as to obtain an analyser for termination inference. Termination checking for logic programs has been studied extensively (see for example the survey @cite_18 ). Backwards reasoning for imperative programs dates back to the early days of static analysis and has been applied extensively in functional programming. Applications of backwards analysis in the context of logic programming are few. For details concerning other applications of backwards analysis, see @cite_14 . The only other work on termination inference that we are aware of is that of Mesnard and coauthors. The implementation of Mesnard's cTI analyser is described in @cite_15 and its formal justification is given in @cite_23 .
@cite_18 @cite_14 @cite_23 @cite_15
2009286786 1999783590 1524883003
Abstract We survey termination analysis techniques for Logic Programs. We give an extensive introduction to the topic. We recall several motivations for the work, and point out the intuitions behind a number of LP-specific issues that turn up, such as: the study of different classes of programs and LP languages, of different classes of queries and of different selection rules, the difference between existential and universal termination, and the treatment of backward unification and local variables. Then, we turn to more technical aspects: the structure of the termination proofs, the selection of well-founded orderings, norms and level mappings, the inference of interargument relations, and special treatments proposed for dealing with mutual recursion. For each of these, we briefly sketch the main approaches presented in the literature, using a fixed example as a file rouge. We conclude with some comments on loop detection and cycle unification and state some open problems. The Constraint Logic Programming (CLP) Scheme merges logic programming with constraint solving over predefined domains. In this article, we study proof methods for universal left termination of constraint logic programs. We provide a sound and complete characterization of left termination for ideal CLP languages which generalizes acceptability of logic programs. The characterization is then refined to the notion of partial acceptability, which is well suited for automatic modular inference. We describe a theoretical framework for automation of the approach, which is implemented. For nonideal CLP languages and without any assumption on their incomplete constraint solvers, even the most basic sound termination criterion from logic programming does not lift. We focus on a specific system, namely CLP(R), by proposing some additional conditions that make (partial) acceptability sound. We present the implementation of cTI, a system for universal left-termination inference of logic programs. Termination inference generalizes termination analysis checking. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided to the system, requiringu ser annotations. With termination inference such annotations are no longer necessary. Instead, all provably terminatingclasses to all related predicates are inferred at once. The architecture of cTI is described1 and some optimizations are discussed. Runningti mes for classical examples from the termination literature in LP and for some middle-sized logic programs are given.