A semantic basis for the termination analysis of logic programs

This paper presents a formal semantic basis for the termination analysis of logic programs. The semantics exhibits the termination properties of a log ic program through its binary unfoldings - a possibly infinite set of binar y clauses. Termination of a program P and goal G is determined by the absen ce of an infinite chain in the binary unfoldings of P starting with G. The result is of practical use as basing termination analysis on a formal seman tics: facilitates both the design and implementation of analyzers. A simple Prolog interpreter for binary unfoldings coupled with an abstract domain b ased on symbolic norm constraints is proposed as an implementation vehicle. We illustrate its application using two recently proposed abstract domains . Both the techniques are implemented using a standard CLP(R) library. The combination of an interpreter for binary unfoldings and a constraint solver simplifies the design of the analyzer and improves its efficiency signific antly. (C) 1999 Elsevier Science Inc. All rights reserved.