Module 3 · Lesson 3

Tail Recursion & Accumulators

Write efficient recursive functions that don't blow the stack. Learn how accumulators transform recursion into iteration.

The Stack Problem

Regular recursion builds up a chain of pending operations on the call stack:

lean

1-- Naive factorial: NOT tail recursive
2def factorial : Nat → Nat
3  | 0 => 1
4  | n + 1 => (n + 1) * factorial n
5
6-- How it executes for factorial 4:
7-- factorial 4
8-- = 4 * factorial 3
9-- = 4 * (3 * factorial 2)
10-- = 4 * (3 * (2 * factorial 1))
11-- = 4 * (3 * (2 * (1 * factorial 0)))
12-- = 4 * (3 * (2 * (1 * 1)))
13-- Stack depth: 5 frames!

⚠

Each recursive call adds a frame to the stack. For large inputs, this causes stack overflow. factorial 100000would crash!

What is Tail Recursion?

A function is tail recursive when the recursive call is thelast operation—nothing happens after it returns.

lean

1-- Tail recursive factorial using an accumulator
2def factorialTail (n : Nat) (acc : Nat := 1) : Nat :=
3  match n with
4  | 0 => acc
5  | n + 1 => factorialTail n (acc * (n + 1))
6
7-- How it executes for factorialTail 4:
8-- factorialTail 4 1
9-- factorialTail 3 4      -- acc = 1 * 4
10-- factorialTail 2 12     -- acc = 4 * 3
11-- factorialTail 1 24     -- acc = 12 * 2
12-- factorialTail 0 24     -- acc = 24 * 1
13-- = 24
14-- Stack depth: 1 frame! (Lean optimizes this)

Key Takeaway

In tail recursion, the recursive call is the final action. The compiler can optimize this to a simple loop, using constant stack space.

The Accumulator Pattern

An accumulator is an extra parameter that carries the result being built. Instead of waiting to combine results after recursion, we combine as we go:

lean

1-- Pattern: Move work INTO the recursive call using an accumulator
2
3-- Non-tail recursive (work AFTER the call)
4def sum : List Nat → Nat
5  | [] => 0
6  | x :: xs => x + sum xs  -- + happens AFTER sum returns
7
8-- Tail recursive with accumulator (work BEFORE the call)
9def sumTail (xs : List Nat) (acc : Nat := 0) : Nat :=
10  match xs with
11  | [] => acc
12  | x :: xs => sumTail xs (acc + x)  -- + happens BEFORE recursive call

Converting to Tail Recursion

Step 1: Identify the Pending Operation

lean

1-- What operation waits for the recursive result?
2def length : List α → Nat
3  | [] => 0
4  | _ :: xs => 1 + length xs  -- The "1 +" waits

Step 2: Add an Accumulator Parameter

lean

1-- Add a parameter to carry the running result
2def lengthTail (xs : List α) (acc : Nat := 0) : Nat :=
3  match xs with
4  | [] => acc
5  | _ :: xs => lengthTail xs (acc + 1)  -- Do the work now!

Step 3: Initialize the Accumulator

lean

1-- Use default parameter or wrapper function
2def length' (xs : List α) : Nat := lengthTail xs 0
3
4-- Or with default parameter (cleaner)
5#eval lengthTail [1, 2, 3, 4, 5]  -- Uses acc = 0 by default

More Examples

Reverse a List

lean

1-- Non-tail recursive (slow: O(n²) due to ++)
2def reverseNaive : List α → List α
3  | [] => []
4  | x :: xs => reverseNaive xs ++ [x]
5
6-- Tail recursive with accumulator (fast: O(n))
7def reverseTail (xs : List α) (acc : List α := []) : List α :=
8  match xs with
9  | [] => acc
10  | x :: xs => reverseTail xs (x :: acc)
11
12#eval reverseTail [1, 2, 3, 4, 5]  -- [5, 4, 3, 2, 1]

Fibonacci

lean

1-- Naive Fibonacci: exponential time!
2def fibNaive : Nat → Nat
3  | 0 => 0
4  | 1 => 1
5  | n + 2 => fibNaive n + fibNaive (n + 1)
6
7-- Tail recursive with TWO accumulators: linear time
8def fibTail (n : Nat) (a : Nat := 0) (b : Nat := 1) : Nat :=
9  match n with
10  | 0 => a
11  | n + 1 => fibTail n b (a + b)
12
13#eval fibTail 50  -- Instant! 12586269025

Deep Dive: How Lean Optimizes Tail Calls

When Lean detects a tail-recursive function, it compiles it to an efficient loop. The transformation looks like:

lean

1-- Your tail-recursive code:
2def sumTail (xs : List Nat) (acc : Nat) : Nat :=
3  match xs with
4  | [] => acc
5  | x :: xs => sumTail xs (acc + x)
6
7-- Becomes something like (conceptually):
8def sumLoop (xs : List Nat) (acc : Nat) : Nat := do
9  let mut xs := xs
10  let mut acc := acc
11  while true do
12    match xs with
13    | [] => return acc
14    | x :: rest => 
15      acc := acc + x
16      xs := rest

This is called tail call optimization (TCO). The recursive call reuses the current stack frame instead of creating a new one.

When Accumulators Change the Result

Sometimes the accumulator builds results in reverse order:

lean

1-- Map without accumulator (correct order, not tail recursive)
2def mapNaive (f : α → β) : List α → List β
3  | [] => []
4  | x :: xs => f x :: mapNaive f xs
5
6-- Map with accumulator (reversed!)
7def mapTailReversed (f : α → β) (xs : List α) (acc : List β := []) : List β :=
8  match xs with
9  | [] => acc
10  | x :: xs => mapTailReversed f xs (f x :: acc)
11
12-- Fix: reverse at the end
13def mapTail (f : α → β) (xs : List α) : List β :=
14  (mapTailReversed f xs []).reverse
15
16#eval mapTail (· * 2) [1, 2, 3]  -- [2, 4, 6]

Continuation-Passing Style (Advanced)

lean

1-- Another technique: pass a continuation function
2def sumCPS (xs : List Nat) (k : Nat → α) : α :=
3  match xs with
4  | [] => k 0
5  | x :: xs => sumCPS xs (fun rest => k (x + rest))
6
7-- Usage
8#eval sumCPS [1, 2, 3, 4, 5] id  -- 15
9
10-- This is tail recursive in the CPS sense!

Practical Guidelines

Use Tail Recursion When:

• Processing large data structures (lists, trees)
• The recursion depth could be very large
• Performance is critical

Naive Recursion is Fine When:

• Data is small and bounded
• Code clarity is more important than performance
• You're writing proofs (structure matters)

💡

Lean's standard library uses tail recursion extensively. Functions likeList.foldl are tail recursive, whileList.foldr is not.

Quick Reference

lean

1-- Template for converting to tail recursion:
2
3-- 1. Original function
4def original (x : Input) : Output := 
5  baseCase | recursiveCase with pendingWork
6
7-- 2. Tail recursive version  
8def tailRec (x : Input) (acc : Output := initialValue) : Output :=
9  match x with
10  | baseCase => acc
11  | recursiveCase => tailRec smallerInput (updateAcc acc)
12
13-- Key insight: move "pendingWork" into "updateAcc"

Recursion Next: Higher-Order Functions