Structural and well-founded recursion

Plain-language version: Functions that always finish· Induction, as the machine sees it

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Lean lets a function be defined by calling itself, but Lean's kernel knows nothing of recursive definitions. Before a recursive definition reaches the Lean kernel, the elaborator replaces the recursion by a non-recursive term built from recursors or from a well-founded fixed-point combinator, and the fact that this translation succeeds is the proof that the function terminates. This page explains why unrestricted recursion is not allowed, how structural recursion is compiled through the recursor, how well-founded recursion is compiled through WellFounded.fix, what termination_by and decreasing_by control, how partial and unsafe definitions are kept from compromising the logic, and the induction principles Lean derives from a recursive definition.

Why recursion must be checked

If any recursive equation were accepted as a definition, the logic would be inconsistent. The equation f n = f n + 1 would define a natural-number function with the absurd property that a number equals its successor; and a function into the empty type Empty that simply calls itself would produce an element of a type with no elements, from which anything follows. A proof that "P holds because P holds" would be accepted. Lean's logic therefore treats every function as total: defined on every argument and returning in finitely many steps.

Termination is not checked by Lean's kernel, which has no termination checker; it is guaranteed because every recursive function is elaborated into uses of primitive recursors, which cannot loop. Elaboration proceeds in two phases. First the definition is elaborated as if the core language had recursion, giving a pre-definition; the compiler generates code from it unchanged. Then a termination analysis translates the pre-definition into a non-recursive term for the Lean kernel. Without an explicit instruction the elaborator tries structural recursion on each argument in turn, and then searches for a decreasing measure for well-founded recursion. The reference manual also describes partial fixpoints and predicates defined as least or greatest fixed points; this page does not treat them.

Structural recursion

A definition is structurally recursive when every recursive call is on a strict sub-term of one fixed argument, the decreasing parameter, as exposed by pattern matching. The Fibonacci function is a standard example:

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

#print fib
example : fib 10 = 55 := rfl

Lean 4.34.1 prints the term the Lean kernel received:

def fib : Nat → Nat :=
fun x => Nat.brecOn x fib._f

There is no self-reference. The recursion has become an application of Nat.brecOn, and the cases of the definition are in an auxiliary function fib._f.

fib calls itself on n, two steps below its argument, so the plain recursor, whose step function sees only the result for the immediate predecessor, does not fit directly. The elaborator uses two constructions derived from the recursor instead. For a motive C, Nat.below t is a table holding a value of C k for every k smaller than t, built as an iterated pair; Nat.brecOn is a recursor whose step function receives that whole table, so it can use the result for any smaller argument. This is course-of-values recursion. Lean generates below and brecOn for every inductive type, following McBride, Goguen and McKinna.

#check @Nat.brecOn
#print fib._f

@Nat.brecOn : {motive : Nat → Sort u_1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t
@[reducible] def fib._f : (x : Nat) → Nat.below x → Nat :=
fun x f =>
  (match (motive := (x : Nat) → Nat.below x → Nat) x with
    | 0 => fun x => 0
    | 1 => fun x => 1
    | n.succ.succ => fun x => x.2.1 + x.1)
    f

In the last case the two recursive calls have become two lookups in the table: x.1 is the entry for n + 1 and x.2.1 the entry for n. Because brecOn and below are themselves defined from Nat.rec, the whole definition reduces by the ordinary rules of definitional equality, which is why fib 10 = 55 holds by rfl. Structurally recursive functions compute inside Lean's kernel, and their defining equations hold definitionally.

The analysis is syntactic, so some terminating functions fail it. A function that tests n == 0 and recurses on n - 1 terminates, but n - 1 is not exposed as a sub-term by any pattern match, so it is not structural; such functions need well-founded recursion. The clause termination_by structural x names the decreasing parameter explicitly and forbids the fallback.

The term built from brecOn is not what runs. Compiled code is generated from the pre-definition with ordinary recursion; the recursor-based term exists to justify termination, not to be executed.

Well-founded recursion

A relation $\prec$ is well-founded when there is no infinite descending chain $x_0\succ x_1\succ x_2\succ \cdots$. Lean states this through the accessibility predicate Acc, an inductive proposition: x is accessible when every y ≺ x is accessible, and a relation is well-founded when every element is accessible. A function whose arguments decrease along a well-founded relation at every recursive call can be defined with the fixed-point combinator

#check @WellFounded.fix

@WellFounded.fix : {α : Sort u_1} →
  {C : α → Sort u_2} → {r : α → α → Prop} → WellFounded r → ((x : α) → ((y : α) → r y x → C y) → C x) → (x : α) → C x

Its step function receives the current argument x and a function that may be called only on arguments y accompanied by a proof of r y x. WellFounded.fix is defined through an auxiliary function, WellFounded.fixF, that takes the accessibility proof as an explicit argument:

#print WellFounded.fixF

def WellFounded.fixF.{u, v} : {α : Sort u} →
  {r : α → α → Prop} → {C : α → Sort v} → ((x : α) → ((y : α) → r y x → C y) → C x) → (x : α) → Acc r x → C x :=
fun {α} {r} {C} F x a => Acc.rec (fun x₁ h ih => F x₁ ih) a

Its body is one application of Acc.rec, the recursor of the accessibility predicate. Well-founded recursion is therefore structural recursion again, on a proof that the arguments decrease rather than on the data. A function's several arguments are packed into a single dependent pair, the relation is pulled back from the measure with invImage, and each recursive call is given its proof of decrease.

The measure is given with termination_by and the proofs of decrease with decreasing_by:

def log2 (n : Nat) : Nat :=
  if h : n < 2 then 0 else 1 + log2 (n / 2)
termination_by n
decreasing_by omega

#eval log2 1024
#print log2

The evaluation prints 10, and #print shows

@[irreducible] def log2 : Nat → Nat :=
WellFounded.Nat.fix (fun x => x) fun n a => if h : n < 2 then 0 else 1 + a (n / 2) ⋯

The recursive call log2 (n / 2) has become a (n / 2) ⋯, where ⋯ stands for the proof, produced by omega, that n / 2 < n in the branch where n is at least 2. Here the measure is a natural number, and since Lean 4.27.0 such definitions use WellFounded.Nat.fix, a variant whose recursion runs on a natural-number "fuel" argument initialised from the measure, which makes the definitions easier to evaluate. For other measures, such as a pair of numbers compared lexicographically, the elaborator produces a term built on WellFounded.fix directly. When decreasing_by is omitted a default tactic tries to prove each obligation.

The @[irreducible] attribute is the visible difference from structural recursion. Definitions by well-founded recursion are irreducible by default, so the elaborator will not unfold them while checking definitional equality, and an equation that would follow by computation is not accepted by rfl:

example : log2 8 = 3 := rfl

Type mismatch
  rfl
has type
  ?m.7 = ?m.7
but is expected to have type
  log2 8 = 3

The equation is still true, and Lean proves the defining equation as a theorem, log2.eq_1, so that simp [log2] can rewrite with it and prove the example. Even when the reductions do hold definitionally, they may be slow in the Lean kernel, which must unfold the proof of termination along with the definition. The reference manual's advice is to use structural recursion, where possible, for functions meant for use in types or wherever definitional equality matters.

Functional induction

A recursive definition determines an induction principle that follows its own case split and recursive calls. Since Lean 4.8.0 the elaborator derives it automatically, as a theorem named f.induct for a recursive function f. It exists for the structurally recursive fib as well as for the well-founded log2:

#check @fib.induct
#check @log2.induct

theorem log2_le (n : Nat) : log2 n ≤ n := by
  fun_induction log2 n with
  | case1 n h => simp
  | case2 n h ih => omega

fib.induct : ∀ (motive : Nat → Prop),
  motive 0 → motive 1 → (∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) → ∀ (a : Nat), motive a
log2.induct : ∀ (motive : Nat → Prop),
  (∀ (x : Nat), x < 2 → motive x) → (∀ (x : Nat), ¬x < 2 → motive (x / 2) → motive x) → ∀ (n : Nat), motive n

Each principle has one case for each branch of its function. For fib the recursive case has two induction hypotheses, one per recursive call: the two-step induction that the definition needs, which ordinary induction on Nat does not supply directly. For log2 the recursive branch carries an induction hypothesis for exactly the argument of the recursive call, x / 2. The fun_induction tactic, added in Lean 4.18.0, applies it to a goal about log2 n.

Partial and unsafe definitions

Two modifiers admit definitions that are not shown to terminate, and both prevent them from compromising proofs.

A partial definition is checked by the Lean kernel for type-correctness as if recursion were allowed, and then enters the logic as an opaque constant: a constant with a type and no definition the Lean kernel may unfold. The compiler still produces ordinary code for it.

partial def collatz (n : Nat) : Nat :=
  if n ≤ 1 then 0 else 1 + collatz (if n % 2 = 0 then n / 2 else 3 * n + 1)

#eval collatz 27
#print collatz

Lean prints 111 and then opaque collatz : Nat → Nat. Whether this function terminates on every input is the open Collatz problem. A partial function may appear in propositions and proofs, but its equational theory is very weak: no property of its values that depends on its definition can be proved, because the logic sees no definition. Even unfolding it fails:

example : collatz 1 = 0 := by unfold collatz; rfl

Lean reports Tactic `unfold` failed to unfold `collatz` in followed by the goal, collatz 1 = 0. For the same reason a partial function's result type must be shown to be inhabited. Otherwise a partial function into Empty would be an opaque constant producing an element of an empty type, and so a proof of anything:

partial def loop (n : Nat) : Empty := loop (n + 1)

is rejected: failed to compile 'partial' definition `loop`, could not prove that the type Nat → Empty is nonempty.

An unsafe definition has none of these restrictions. It may recurse freely, its type need not be inhabited, and it may use operations, such as unchecked casts between types, that break the equational theory. In exchange it may be used only by other unsafe definitions, and never in a theorem:

unsafe def spin (n : Nat) : Empty := spin (n + 1)

theorem oops : False := (spin 0).elim

Lean reports (kernel) invalid declaration, it uses unsafe declaration 'spin'. The prefix shows that the refusal is made by Lean's kernel itself, so it does not depend on the elaborator being correct. partial and unsafe thus mark the boundary between Lean as a programming language, where non-termination is a fact of life, and Lean as a logic, where it would be a contradiction.

Next

Definitional equality describes the computation rules that structural recursion relies on and that irreducible definitions withhold, and how Lean's kernel decides them.