← CatZep/Engineering Guides/The Science of Programming

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.

Concepts explained in this guide

Read these definitions first, or use the linked terms as you go. The examples and limitations are local to this guide; companion pages are optional.

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:

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.

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

# {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:

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:

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.

# {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)}

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

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:

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

Worked example: factorial by recursion and accumulator

Work through the state changes and the exact claim being checked.

Run and change the example

Download guide_labs.py. Python 3.10+, standard library only. In its directory, run:

python3 guide_labs.py recursion
python3 guide_labs.py test

The complete standard-library lab checks the stated finite cases and boundary inputs. Its invariants explain the reasoning; tests alone do not prove all possible inputs.

The program tests its stated finite contracts. It is an educational model, not an implementation of the named production product or a proof of unmodeled distributed faults.

Summary