Quasi-Terminating Logic Programs for Ensuring the Termination of Partial Evaluation

Abstract. A logic program strongly quasi-terminates when only a finite number of distinct atoms (modulo variable renaming) are derivable from any given query and computation rule. This notion of quasi-termination, though stronger than related notions that only consider Prolog’s computation rule, is essential for ensuring the termination of partial evaluation, where liberal selection policies are often mandatory to achieve a good specialization. In this paper, we introduce sufficient conditions for the strong termination and quasi-termination of logic programs which are based on the construction of size-change graphs. The class of strongly quasi-terminating logic programs, however, is too restricted. Therefore, we also introduce an annotation procedure that annotates those predicate arguments which are responsible of the non-quasi-termination. As a consequence, the annotated program behaves like a quasi-terminating program if annotated arguments are generalized (i.e., replaced by a fresh variable) when they occur in a computation. We illustrate the usefulness of our approach by designing a simple partial evaluator in which global termination is always ensured offline (i.e., statically). A prototype implementation demonstrates its viability.