Module 3 · Lesson 2

Recursion

Recursion is the primary looping mechanism in Lean. Unlike imperative loops, recursive functions must be provably terminating.

Structural Recursion

The simplest form of recursion follows the structure of the data:

lean

1-- Recursion on Nat
2def factorial : Nat → Nat
3  | 0 => 1
4  | n + 1 => (n + 1) * factorial n
5
6-- Recursion on List
7def length : List α → Nat
8  | [] => 0
9  | _ :: xs => 1 + length xs
10
11-- Recursion on custom type
12inductive Tree where
13  | leaf
14  | node (left : Tree) (value : Nat) (right : Tree)
15
16def Tree.size : Tree → Nat
17  | leaf => 0
18  | node left _ right => 1 + left.size + right.size
19
20#eval factorial 5  -- 120
21#eval length [1, 2, 3, 4]  -- 4

In each case, the recursive call is on a "smaller" value—a predecessor of a Nat, the tail of a List, or a subtree. This guarantees termination.

Termination Checking

Lean requires proof that all functions terminate. For structural recursion, this is automatic. But some patterns need help:

lean

1-- This works: clearly structural
2def sum : List Nat → Nat
3  | [] => 0
4  | x :: xs => x + sum xs
5
6-- This needs a hint: n / 2 is smaller, but Lean can't see it
7def collatz (n : Nat) : Nat :=
8  if n ≤ 1 then n
9  else if n % 2 == 0 then collatz (n / 2)
10  else collatz (3 * n + 1)
11termination_by n
12decreasing_by sorry  -- We're cheating here—Collatz termination is unproven!

⚠

The Collatz conjecture is famously unproven in mathematics! We use sorry here to skip the proof. In real code, you'd need to prove termination or use partial.

Partial Functions

When you can't prove termination (or don't want to), use partial:

lean

1-- A server loop that runs forever
2partial def serverLoop (state : ServerState) : IO Unit := do
3  let request ← readRequest
4  let newState ← handleRequest state request
5  serverLoop newState  -- Infinite recursion is OK with partial
6
7-- Reading user input until valid
8partial def getValidInput : IO Nat := do
9  IO.println "Enter a positive number:"
10  let input ← IO.getLine
11  match input.trim.toNat? with
12  | some n => return n
13  | none => 
14    IO.println "Invalid input, try again."
15    getValidInput

Key Takeaway

Use partial for functions that intentionally don't terminate (servers, REPLs) or when proving termination is too complex. Regular defrequires termination proof.

Tail Recursion

Tail-recursive functions are optimized to use constant stack space:

lean

1-- NOT tail recursive: has pending work after recursive call
2def factorialBad : Nat → Nat
3  | 0 => 1
4  | n + 1 => (n + 1) * factorialBad n  -- Must multiply AFTER the call
5
6-- Tail recursive: uses an accumulator
7def factorialGood (n : Nat) : Nat :=
8  go n 1
9where
10  go : Nat → Nat → Nat
11  | 0, acc => acc
12  | n + 1, acc => go n ((n + 1) * acc)  -- Recursive call is last
13
14-- Both compute the same result
15#eval factorialBad 10   -- 3628800
16#eval factorialGood 10  -- 3628800

The tail-recursive version won't overflow the stack even for large inputs.

Common Recursive Patterns

Map: Transform Each Element

lean

1def map (f : α → β) : List α → List β
2  | [] => []
3  | x :: xs => f x :: map f xs
4
5#eval map (· * 2) [1, 2, 3]  -- [2, 4, 6]

Filter: Keep Matching Elements

lean

1def filter (p : α → Bool) : List α → List α
2  | [] => []
3  | x :: xs => if p x then x :: filter p xs else filter p xs
4
5#eval filter (· > 2) [1, 2, 3, 4, 5]  -- [3, 4, 5]

Fold: Accumulate a Result

lean

1def foldl (f : β → α → β) (init : β) : List α → β
2  | [] => init
3  | x :: xs => foldl f (f init x) xs
4
5#eval foldl (· + ·) 0 [1, 2, 3, 4, 5]  -- 15

Deep Dive: Well-Founded Recursion

Beyond structural recursion, Lean supports "well-founded recursion" where you prove that some measure decreases on each call:

lean

1def gcd (m n : Nat) : Nat :=
2  if n = 0 then m
3  else gcd n (m % n)
4termination_by n  -- n decreases each iteration

The termination_by clause tells Lean what to track. Here,m % n is always less than n, so termination is guaranteed.

Mutual Recursion

Functions that call each other use mutual:

lean

1mutual
2  def isEven : Nat → Bool
3    | 0 => true
4    | n + 1 => isOdd n
5
6  def isOdd : Nat → Bool
7    | 0 => false
8    | n + 1 => isEven n
9end
10
11#eval isEven 4  -- true
12#eval isOdd 7   -- true

Recursion vs Iteration

Lean provides for loops in the do notation, but they're syntactic sugar for recursion:

lean

1-- Imperative-looking but actually recursive
2def sumArray (arr : Array Nat) : Nat := Id.run do
3  let mut total := 0
4  for x in arr do
5    total := total + x
6  return total
7
8-- Equivalent explicit recursion
9def sumArray' (arr : Array Nat) : Nat :=
10  arr.foldl (· + ·) 0
11
12#eval sumArray #[1, 2, 3, 4, 5]  -- 15

Pattern Matching Next: Higher-Order Functions