A Semantic Basis for the Termination Analysis of Logic Programs

The Journal of Logic Programming; 41 (1): 103-123, 1999

Abstract:

This paper presents a declarative semantics which exhibits the termination properties of a logic program. The semantics associates a program with its binary unfoldings --- a possibly infinite set of binary clauses. Termination of a program P and goal G is indicated by the absence of an infinite chain in the binary unfoldings of P starting with G. The main contribution is a formal semantic basis for the termination analysis of logic programs which facilitates both design and implementation. As an implementation vehicle we propose a simple meta-interpreter for binary unfoldings and the use of an abstract domain based on symbolic norm constraints. Many of the recently proposed termination analyses for logic programs can be expressed concisely within our approach. To demonstrate our approach we have reformulated the analysis originally described in ite{LinSag}. The implementation uses a standard library for linear equations over the reals. The combination of binary unfoldings and a constraint solver is shown to significantly simplify the design of the analysis.

Available: bibtex entry compressed postscript

Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il