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
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.