1.4. From Recursion to Imperative Loops¶
- File:
Loops.ml
The way the auxiliary function walk
function find_min has been
implemented is known as tail-call-recursion: each recursive call
happens to be the very last thing the function does in a non-base
(recursive) case.
Due to this structure, which leaves “nothing to do” after the
recursive call, a tail-recursive function can be transformed to an
imperative while
-loop. The benefits of such transformation is the
possibility not to use the Call Stack, necessary to stall the
calling structure of the program, but rather keep the computation
“flat”.
The transformation of a tail-recursive program into a program that
uses the while
-loop happens in two phases:
- Make the parameters of the functions mutable references, so they could be re-assigned at each loop iteration.
- Make the branch-condition of “base” case to be that of the
while
-loop. Whatever post-processing of the result takes place in the base cases, should now be done after the loop.
The result of transforming find_min into a loop is as follows:
let find_min_loop ls =
let loop cur_tail cur_min =
while !cur_tail <> [] do
let xs = !cur_tail in
let h = List.hd xs in
let min = !cur_min in
cur_min := if h < min then h else min;
cur_tail := List.tl xs
done;
!cur_min
in match ls with
| h :: t ->
let cur_tail = ref t in
let cur_min = ref h in
let min = loop cur_tail cur_min in
Some min
| _ -> None
Notice that the function walk
has been renamed loop
, which is
no longer recursive: the tail recursion has been “unfolded” into the
loop, and pattern-matching has been replaced by the loop condition
!cur_tail <> []
. Furthermore, all parameters are now just
references that are being reassigned at each loop iteration.
An important observation is that reassigning the mutable variables in an imperative implementation is equivalent to passing new arguments in the corresponding recursive implementation. Knowing that makes it easy to “switch” between loop-based imperative and tail-recursive functional implementations.
1.4.1. Loop variants¶
The function find_min_loop
still terminates. The main source of
non-termination in imperative programs, in addition to recursion, are
loops. However, we can reason about the loop termination in the same
way we did for recursive programs: by means of finding a loop
variant (i.e., termination measure), expressed as a function of
values stored in variables, affected by the loop iteration.
In the case of loop
above the loop variant is the size of a list
stored in the variable cur_tail
, which keeps decreasing, leading
to the loop termination when the it becomes zero.
1.4.2. Loop invariants¶
Now, as we have a program with a loop, can we use the same methodology to ensure its correctness using pre- and postconditions? The answer is yes, and, in fact, we are only going to need the definitions that we already have.
The precondition of what used to be walk
and is now loop
becomes loop invariant, which serves exactly the same purpose as the
precondition of a recursive version. Specifically, it should
- be true before and after each iteration;
- when conjoined with the loop condition, allow for establishing the property of the loop-affected state, implying the client-imposed specification.
Notice that the first quality of the loop invariant is the same as of the precondition. The fact that it must hold not just at the beginning, but also at the end of each iteration is because in a loop, a new iteration begins right after the previous one ends, and hence it expects its “precondition”/”invariant” to hold. The second quality corresponds to the intuition that the invariant/precondition should be chosen in a way that when a loop terminates (or, equivalently, a recursive function returns), the invariant allows to infer the postcondition.
All that said, for our imperative version of finding a minimum, we can
use find_min_walk_pre
as the loop invariant, annotating the
program as follows:
let find_min_loop_inv ls =
let loop cur_tail cur_min =
(* The invariant holds at the beginning of the loop *)
assert (find_min_walk_pre ls !cur_tail !cur_min);
while !cur_tail <> [] do
let xs = !cur_tail in
let h = List.hd xs in
let min = !cur_min in
cur_min := if h < min then h else min;
cur_tail := List.tl xs;
(* The invariant holds at the end of the iteration *)
assert (find_min_walk_pre ls !cur_tail !cur_min);
done;
!cur_min
in match ls with
| h :: t ->
let cur_tail = ref t in
let cur_min = ref h in
(* The invariant holds at the beginning of the loop *)
assert (find_min_walk_pre ls !cur_tail !cur_min);
let min = loop cur_tail cur_min in
(* Upon finishing the loop, the invariant implies the postcondition. *)
assert (find_min_walk_post ls !cur_tail !cur_min min);
Some min
| _ -> None