What does "loops must be folded to ensure termination" mean?

Question

I came across "loops must be folded to enusre termination" in a paper on formal methods (abstract interpretation to be precise). I am clear on what termination means, but I do not know what a folded loop is, nor how to perform folding on a loop.

Could someone please explain to me what a folded loop is please? And if it is not implicit in, or does not follow immediately for the definition of a folded loop, how this ensures termination?

Thanks

Answer 1

I have no knowledge of abstract interpretation, so I'll take the functional programming approach to folding. :-)

In functional programming, a fold is an operation applied to a list to do something with each element, updating a value each iteration. For example, you can implement map this way (in Scheme):

(define (map1 func lst)
  (fold-right (lambda (elem result)
                (cons (func elem) result))
              '() lst))

What that does is that it starts with an empty list (let's call that the result), and then for each element of the list, from the right-hand-side moving leftward, you call func on the element and cons its result onto the result list.

The key here, as far as termination goes, is that with a fold, the loop is guaranteed to terminate as long as the list is finite, since you're iterating to the next element of the list each time, and if the list is finite, then eventually there will be no next element.

Contrast this with a more C-style for loop, that doesn't operate on a list, but instead have the form for (init; test; update). The test is not guaranteed to ever return false, and so the loop is not guaranteed to complete.

Answer 2

Folding a loop is the opposite action from the better-known loop unfolding, which itself is better known as loop unrolling. Given a loop, to unfold it means to repeat the body several times, so that the loop test is executed less often. When the number of executions of the loop in advance, the loop can be completely unfolded, leaving a simple sequence of instructions. For example, this loop

for i := 1 to 4 do
  writeln(i);

can be unfolded to

writeln(1);
writeln(2);
writeln(3);
writeln(4);

See C++ loop unfolding, bounds for another example with partial unfolding.

The metaphor is that the program is folded on itself many times over; unfolding means removing some or all of these folds.

In some static analysis techniques, it is difficult to deal with loops, because finding a precondition for the entry point of the loop (i.e. finding a loop invariant) requires a fixpoint computation which is unsolvable in general. Therefore some analyses unfold loops; this requires having a reasonable bound on the number of iterations, which limits the scope of programs that can be analyzed.

In other static analysis techniques, finding a good invariant is a critical part of the analysis. It doesn't help to unfold the loop, in fact partially unfolding the loop would make the loop body larger and so would make it more difficult to determine a good invariant; and completely unfolding the loop would be impractical or impossible if the number of iterations was large or unbounded. Without seeing the paper, I find the statement a bit surprising, because the code could have been written with the unfolded form, but there can be programs that the analysis only works on in a more folded form.