This paper presents a formal semantic basis for the termination analysis of logic programs. The semantics exhibits the termination properties of a logic program through its binary unfoldings | a possibly in nite set of binary clauses. Termination of a program P and goal G is determined by the absence of an in nite chain in the binary unfoldings of P starting with G. The result is of practical use as basing termination analysis on a formal semantics facilitates both the design and implementation of analyzers. A simple Prolog interpreter for binary unfoldings coupled with an abstract domain based on symbolic norm constraints is proposed as an implementation vehicle. We illustrate its application using two recently proposed abstract domains. Both techniques are implemented using a standard CLP(R) library. The combination of an interpreter for binary unfoldings and a constraint solver simpli es the design of the analyzer and improves its e ciency signi cantly.
First, the termination engine of REF is used to compute a set of binary clauses which describe possible loops in the program with size relations.
A Semantic Basis for the Termination Analysis of Logic Programs
Journal of Logic Programming
Computer Science