Suppose we execute a program with only some of the data it needs. If we reach a choice point requiring data we do not have, we could return a program consisting of the choice test and the code used in its branches. We could go further and return a program where the code for each of the branches comes from similar execution. This is partial evaluation. The result is a program that would be more efficient than the original when we know the data has the aspects fed into the partial evaluation.

If we encounter a recursive call with arguments different from those of the original call we are partially evaluating, we have a problem. Continuing with the partial evaluation of this call could give another recursive call and so on infinitely, but if we leave it unevaluated we may miss opportunities for further efficiency improvements.

Determining when to terminate in these circumstances is a big issue. This paper undertakes a formal analysis, the underlying principle being that we can continue with the partial evaluation if the data in the recursive call is in some provable sense smaller than the data in the original call.

As in much work in partial evaluation, the language used is Prolog, which is particularly amenable to the technique. It would have been useful if the authors had provided more discussion on the extent to which their analysis techniques are purely oriented toward Prolog or could be applied to other programming languages.