Iteration Instead of Recursion

A recursive mathematical definition is a clean specification; the engineering question is how to compute it with a loop. Gries shows that the recursive definition itself hands you the loop invariant — and where it does not, an explicit stack fills the gap. Throughout, the loop invariant and the induction hypothesis turn out to be the same idea wearing different clothes.

Recursion and iteration are two ways to compute the same function, and Gries treats them as duals rather than rivals. A function defined by a recurrence — a base case plus a rule that reduces a problem to a smaller one — is often the clearest specification you can write. But a straightforward recursive implementation carries call-stack cost and, for deep problems, risks stack overflow. This page works through how to turn a recurrence into a loop: read the recurrence as an invariant, introduce accumulators whose meaning is the invariant for tail recursion, and simulate the call stack explicitly when the recursion forks into two calls. The payoff is the recurring lesson of the book — that a loop invariant corresponds exactly to an inductive hypothesis, and a bound function to the decreasing argument of the recursion.

This is an original study summary for quick reference. Notation follows Gries and Dijkstra: wp for weakest precondition, {P} S {Q} for a Hoare triple, guarded commands (if…fi, do…od) for the programming language. See the book for the full, rigorous treatment.

Contents

  1. Recursive definitions as specifications
  2. Tail recursion → loop directly
  3. From recurrence to invariant
  4. General recursion needs an explicit stack
  5. Why bother
  6. The duality
  7. Summary

Recursive definitions as specifications

Many functions are most honestly described by a recurrence: a base case, and a rule expressing the value at n in terms of the value at a smaller argument. The factorial is the textbook example:

f(0) = 1
f(n) = n · f(n−1)  for n > 0

This definition is a specification, not yet a program. It is complete, unambiguous, and manifestly correct — every value is pinned down and the definition is well-founded because the argument strictly decreases toward the base case. Read as code it is already a recursive function, but the interesting engineering question Gries poses is different: how do we compute this value with a loop, and how do we know the loop is right?

The key insight is that the recurrence tells you what the loop invariant should be. A loop computes the same answer by building it up incrementally, and the “partial answer so far” that a loop maintains is exactly a slice of the recurrence. Where the recursion peels one factor off at a time on the way down and multiplies on the way back up, the loop accumulates those same factors as it counts — and the statement of what has been accumulated is the invariant. So converting recursion to iteration is not guesswork: you read the invariant off the mathematical definition.

# The recurrence, read three ways:
#   as a spec       : f(0)=1, f(n)=n*f(n-1)      (what is true)
#   as a recursion  : return 1 or n*fact(n-1)    (compute down then up)
#   as a loop       : accumulate factors 1,2,...,n   (build up)
# The loop's invariant is a running statement of what has been built.

Tail recursion → loop directly

A function is tail-recursive when the recursive call is the very last thing it does — there is no pending work waiting for the call to return. Such a function carries all of its state forward in its arguments, typically in an accumulator. That structure maps to a while-loop mechanically, and the crucial point is this: the meaning of the accumulator is the loop invariant.

Take factorial written in tail form with an accumulator acc and a counter i. On each step it multiplies acc by i and moves on. The invariant states precisely what acc holds part-way through: it is the product of the factors already consumed. Combined with the remaining work, it must always reconstruct the full answer.

✗ Recursive form — simple, but grows the call stack
# Direct from the recurrence.
# pre:  n ≥ 0     post: returns n!
def fact(n):
    if n == 0:
        return 1
    return n * fact(n - 1)
# n stack frames deep before the
# first multiply happens (non-tail:
# the * waits for the call to return).

# Tail-recursive variant (accumulator):
def fact_t(i, acc):
    if i == 0:
        return acc
    return fact_t(i - 1, acc * i)
# now nothing waits — the call is last.
✓ Iterative form — the accumulator's meaning is the invariant
# {n ≥ 0}
acc := 1 ;  i := 1 ;
# invariant P: acc = (i-1)!   and   1 ≤ i ≤ n+1
#   i.e. acc holds the product of 1..(i-1),
#   and  acc * (i * (i+1) * ... * n) = n!
# bound     t: n - i + 1
do i ≤ n →
     acc := acc * i ;
     i   := i + 1
od
# guard false: i = n+1, so P gives acc = n!  ✓
# {acc = n!}

Check the five loop obligations against the invariant P: acc = (i−1)!. Init: acc=1, i=1 gives acc = 0! = 1 ✓. Preserve: if acc = (i−1)! then after acc := acc*i; i := i+1 we have acc = (i−1)!·i = i! and the counter is now i+1, so acc = ((i+1)−1)! holds again ✓. Exit: ¬B is i = n+1, so acc = n! ✓. Bound: t = n−i+1 is positive while i ≤ n and drops by one each step, forcing termination ✓. The accumulator invariant did all the work: it is nothing more than the recurrence, frozen at the moment the loop has processed the first i−1 factors.

From recurrence to invariant

The factorial pattern generalises into a recipe. Whenever a function is defined by a recurrence that reduces a problem to a smaller one, introduce one or more accumulator variables and state an invariant of the shape:

answer = (combination of the accumulated result so far) with (the remaining work)

The loop advances by folding a piece of the remaining work into the accumulator while preserving that equation. When the remaining work is empty (the guard goes false), the accumulator alone equals the answer. Three canonical cases:

FunctionRecurrenceAccumulator(s) & invariant
Sum 0..ns(0)=0, s(n)=n+s(n−1)s, with P: s = 0+1+…+(i−1); after the loop s = 0+…+n.
Power b^np(0)=1, p(n)=b·p(n−1)p, with P: p = b^(i−1) ∧ p·b^(n−i+1) = b^n.
Fibonaccifib(0)=0, fib(1)=1, fib(k)=fib(k−1)+fib(k−2)carry two values a,b with P: a = fib(k) ∧ b = fib(k+1).

Fibonacci is the instructive one, because a naive recursion recomputes subproblems and costs exponential time. Its recurrence depends on the two previous values, so the accumulator is a pair. The invariant a = fib(k) ∧ b = fib(k+1) says exactly what the two carried variables mean at step k; one iteration slides the window forward by recombining them.

✓ Fibonacci by iteration — carry two previous values
# {n ≥ 0}   post: b0 = fib(n)
a := 0 ;  b := 1 ;  k := 0 ;
# invariant P: a = fib(k) and b = fib(k+1)
#              and 0 ≤ k ≤ n
# bound     t: n - k
do k ≠ n →
     # fib(k+2) = fib(k+1) + fib(k)
     a, b := b, a + b ;   # simultaneous
     k := k + 1
od
# k = n → a = fib(n)
# {a = fib(n)}
✓ Why the pair-invariant is preserved
# before body: a = fib(k), b = fib(k+1)
# new a = old b        = fib(k+1)
# new b = old a + old b
#       = fib(k) + fib(k+1)
#       = fib(k+2)
# with k' = k+1:
#   new a = fib(k')     ✓
#   new b = fib(k'+1)   ✓  invariant restored
# bound n-k drops by 1 each step > 0 ✓ halts
# Cost: O(n) time, O(1) space — vs the
# exponential recomputation of naive recursion.

The general recipe, then: look at what the recurrence depends on. If it needs the immediately preceding value, carry one accumulator; if it needs the two preceding values, carry two; and state the invariant as “these carried variables equal these specific terms of the sequence.” The loop body is forced — it is whatever recombination the recurrence prescribes.

General (non-tail) recursion needs an explicit stack

Tail recursion converts to a bare loop because there is no pending work to remember. General recursion is different. When a function makes two (or more) recursive calls — tree traversal, quicksort, any divide-and-conquer — work remains after the first call returns: the second call, and the combining step. That pending work is precisely what the machine’s call stack holds for you. To iterate, you must simulate the call stack with an explicit stack data structure.

Consider inorder traversal of a binary tree, whose recursive form is traverse(left); visit(node); traverse(right) — two recursive calls straddling a visit. The iterative version keeps an explicit stack of nodes whose left subtrees are still being descended, so it can come back to visit them and then turn right.

# Recursive (for reference):
#   inorder(t): if t != null: inorder(t.left); visit(t); inorder(t.right)

# Iterative inorder with an explicit stack S
# invariant: S holds exactly the ancestors of the
#   'cur' subtree whose own value + right subtree are
#   STILL TO BE VISITED, deepest-pending on top.
#   Everything already popped-and-visited is done in order.
S   := empty stack ;
cur := root ;
do cur ≠ null  or  ¬empty(S) →
     if cur ≠ null →             # descend left, remembering the node
          push(S, cur) ;
          cur := cur.left
     [] cur = null →             # left done: visit, then go right
          cur := pop(S) ;
          visit(cur) ;
          cur := cur.right
     fi
od
# exit: cur = null and S empty → every node visited in order.

The stack is the reification of the recursion’s frames: each push corresponds to entering a recursive call, each pop to returning from one. Preorder is the same shape with the visit moved to push time:

# Iterative preorder: visit on the way down, stack the right child
# invariant: S holds the roots of subtrees not yet traversed,
#   in the order they must be processed (next on top);
#   all nodes already popped have been visited in preorder.
S := empty stack ;  push(S, root) ;
do ¬empty(S) →
     n := pop(S) ;
     if n ≠ null →
          visit(n) ;
          push(S, n.right) ;   # pushed first, popped last
          push(S, n.left)      # pushed last,  popped first → visited next
     [] n = null → skip
     fi
od
# exit: S empty → all reachable nodes visited in preorder.

The invariant in both cases is a statement about the stack contents: the stack holds exactly the pending work — the nodes still to be visited (or descended) — in the correct order, and everything already popped has been processed correctly. Termination follows because every node is pushed and popped at most once, so a bound function counting “nodes not yet pushed plus entries on the stack” strictly decreases. When you cannot fold the recursion into a single accumulator, you make the deferred work explicit, and the stack’s invariant replaces the tidy accumulator invariant of the tail-recursive case.

Why bother

If recursion is often clearer, why convert it? The trade is real and cuts both ways — the point is to choose deliberately rather than by habit.

DimensionIterationRecursion
Call-stack overheadNone — no per-call frame; one activation reused across all steps.One stack frame per pending call; constant-factor cost on every step.
Deep problemsSafe — loop depth is unbounded by the runtime; won’t overflow.Risks stack overflow once depth exceeds the runtime limit.
ClarityCan obscure the structure, especially when an explicit stack is needed.Often the clearest expression — mirrors the recurrence directly.
SpaceTail case: O(1) extra. Explicit-stack case: O(depth), same as recursion but on the heap.O(depth) on the call stack, implicitly.
Correctness reasoningLoop invariant + bound function.Induction on the decreasing argument.

The last row is the deep one and the theme of the next section: the two reasoning methods are not merely analogous, they are the same argument. A loop invariant is an inductive hypothesis; proving the loop preserves it is proving the induction step. So converting recursion to iteration never throws the correctness argument away — it re-expresses it. Choose iteration when depth or per-call cost matters (production code walking large or deep structures), and keep recursion when the recurrence is the clearest possible statement of intent.

The duality

Gries’ unifying observation is that iteration and recursion are proved correct by dual halves of the same well-founded induction. Line them up and the correspondence is exact:

loop invariant  ⟷  induction hypothesis
bound function  ⟷  the decreasing argument of the recursion
“body preserves P”  ⟷  “the inductive step”
“init establishes P” / exit  ⟷  the base case

The loop invariant is what you assume holds at the start of each iteration and must re-establish at the end — identical in role to the induction hypothesis, which you assume for the smaller case and use to conclude the larger. The bound function, a non-negative integer that strictly decreases per iteration, is exactly the decreasing argument that makes a recursion well-founded and guarantees it bottoms out; both appeal to the same principle — there is no infinite strictly-decreasing sequence of natural numbers. Proving a loop and proving the corresponding recursion by induction are therefore the same work, discharged in the same steps, whichever form you write. (See bound functions for the termination argument and developing programs for inventing invariants.)

The consequence: you never have to re-derive correctness when you translate between the two forms. If you have proved the recursion by induction, you already have the loop invariant — it is the induction hypothesis, stated over the accumulated state. If you have proved the loop, you have the inductive argument for the recursion. The choice between iteration and recursion becomes purely about cost and clarity, because the proof is shared.

Summary

IdeaThe one-line takeaway
Recurrence as specA base case plus a reduction rule (e.g. f(0)=1, f(n)=n·f(n−1)) is a clean, well-founded specification; the recurrence suggests the loop invariant.
Tail recursion → loopA tail-recursive function maps to a while-loop with an accumulator; the accumulator’s meaning is the invariant.
Recurrence → invariantIntroduce accumulators; state answer = accumulated-so-far combined with remaining-work. Fibonacci carries two values: a=fib(k) ∧ b=fib(k+1).
General recursionTwo recursive calls (trees, quicksort) need an explicit stack simulating the call stack; its invariant: the stack holds exactly the work still to do.
Why iterateAvoids per-call overhead and stack-overflow on deep problems; recursion is often clearer. Pick deliberately.
The dualityLoop invariant ⟷ induction hypothesis; bound function ⟷ the decreasing recursion argument. Same proof, two forms.
The recurring theme: the invariant and the induction hypothesis are one idea. A recurrence hands you a specification and, with it, the invariant of the loop that computes it; tail recursion becomes a loop with an accumulator, forked recursion becomes a loop with an explicit stack, and in every case the correctness argument is a well-founded induction driven by a decreasing bound. See developing programs & inventing invariants for finding the invariant, bound functions for termination, and the procedure call for how recursion itself is specified and proved.