Inferring and compiling termination for constraint logic programs

Abstract

This paper presents an automated method that deals with termination of constraint logic programs in two steps. First, from the text of a program, the method infers a set of potentially terminating classes using abstract interpretation and boolean mu-calculus. By “potentially”, we roughly mean that for each of these classes, one can find a static order over the literals of the clauses of the program to ensure termination. Then, given a terminating class among those computed at the first step, the second step consists of a “compilation” (or transformation) of the original program to another one by reordering literals. For this new program, the universal left-termination of any query of the considered class is guaranteed. The method has been implemented.