Proving Termination One Loop at a Time

The 13th Workshop on Logic Programming Environments; 2003

Abstract:

Classic techniques for proving termination require the identification of a measure that maps program states to the elements of a well-founded domain. Termination is guaranteed if this measure is shown to decrease with each iteration of a loop in the program. This is a mph{global} termination condition --- there exists a measure which is shown to decrease over all of the loops in the program. In recent years, systems based on mph{local} termination conditions are emerging. Here, termination is guaranteed if for every loop there exists a measure which decreases as execution follows through that loop. In this paper we question the relationship between the two approaches. Reasoning locally is more convenient. But is the local approach really more powerful? We show that for a large class of termination problems the two approaches are equally powerful. To this end we demonstrate that given local conditions which support a proof of termination, a corresponding global condition can always be constructed. On the one hand, the local conditions are simpler and easier to find. Yet on the other hand, in the local approach one must consider a closure operation on loops which may require to consider an exponential number of local conditions.

Available: bibtex entry postscript

Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel
mcodish@cs.bgu.ac.il