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

One of the most important challenges in partial evaluation is the design of automatic methods for ensuring the termination of specialisation. It is well known that the termination of partial evaluation can be ensured when the considered computations are quasiterminating, i.e., when only finitely many different calls occur. In this work, we adapt the use of the so called size-change graphs to logic programming and introduce new sufficient conditions for strong (i.e., w.r.t. any computation rule) termination and quasi-termination. To the best of our knowledge, this is the first sufficient condition for the strong quasi-termination of logic programs. The class of strongly quasi-terminating logic programs, however, is too restrictive. Therefore, we also introduce an annotation procedure that combines the information from size-change graphs and the output of a traditional binding-time analysis. Annotated programs can then be used to guarantee termination of partial evaluation. We finally illustrate the usefulness of our approach by designing a simple partial evaluator in which termination is always ensured offline (i.e., statically)