Lean theorem prover/Explainers/Functions that always finish

Technical version: Structural and well-founded recursion

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

Every function defined inside Lean's logic must finish: given any input, it must return an answer after finitely many steps. This page says why that rule exists, how Lean checks it, and what becomes of a program that might run for ever.

Why a loop would be a proof

In Lean a definition is more than a recipe for computing. It is also an equation the logic may use in proofs. Write a definition that says "the answer for n is the answer for n, plus one", and you have asked the logic to accept that some number equals itself plus one. No natural number does. If the equation were admitted, Lean could prove a false statement, and from one false statement every statement follows. The whole system would be worthless.

So Lean refuses the definition:

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

Lean 4.34.1 begins its reply with fail to show termination for, names loop, and gives its reason: the argument n "is unchanged in the recursive calls". Nothing gets smaller, so nothing guarantees an end. The Lean Language Reference states the danger directly: unrestricted recursion would make Lean's logic inconsistent, because it would allow a circular proof, one that says a statement holds because it holds.

Why Lean cannot just watch for loops

A natural idea is to let the computer inspect each definition and decide whether it always finishes. That cannot be done in general. In 1936 Alan Turing showed that no mechanical procedure can settle, for every machine, questions of this kind, such as whether a given machine will ever print a certain symbol. The best-known form of the result, the halting problem, asks whether a program stops; it too has no general solution.

So Lean does not try to decide termination. It asks the author for a reason it can check, and it accepts two kinds of reason.

Reason one: the input gets smaller

Many functions call themselves only on a piece of their input. The factorial is the standard case:

def fact : Nat → Nat
  | 0     => 1
  | n + 1 => (n + 1) * fact n

#eval fact 20

Lean prints 2432902008176640000.

A natural number in Lean is zero with some number of "plus ones" stacked on it (see building things from constructors). The second line of the definition handles a number of the form n + 1 by calling fact on n, which has one layer fewer. Every number has finitely many layers, so the calls must reach zero. This is called structural recursion: each call works on a strict part of the input. Lean recognises it without help. It translates the definition into the recursion principle that comes with the type of natural numbers, and the Lean kernel then needs no separate test for termination, only its ordinary check of types.

Reason two: a measure goes down

Some functions shrink their input in a way that is not "taking a piece". This one counts how many times a number can be halved before it falls below 2:

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

#eval halvings 1000

Lean prints 9.

Half of a number is not one of its layers, so structural recursion does not apply. The line termination_by n names a measure: a quantity, here the number itself, that must be smaller at every recursive call. Lean then sets a small proof obligation for each call. Here the obligation is n / 2 < n, to be shown knowing that n < 2 is false. The line decreasing_by omega supplies the proof, using an arithmetic procedure described in automation and its limits. When decreasing_by is left out, Lean tries a default procedure of its own. This is well-founded recursion: there is no endless descending chain of natural numbers, so a measure that falls at every step must stop.

The two kinds differ in cost. A function defined by structural recursion computes readily inside the logic. One defined by well-founded recursion often does not, because the checker must work through the proof of termination as well; the Lean Language Reference warns that such functions are frequently slow to compute with (see computation inside proofs).

Programs that may never finish

Some programs are useful even though nobody can prove that they stop. Start with a positive whole number; halve it if it is even, otherwise triple it and add one; repeat until you reach 1. Whether every starting number reaches 1 is the 3x+1 problem, also called the Collatz problem, and it is unsolved. A function that counts the steps can be written, but no proof that it always finishes is known. Lean accepts it when it is marked partial:

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

#eval collatz 27
#print collatz

The program runs: #eval prints 111. But #print shows what the logic sees: opaque collatz : Nat → Nat. To the logic, a partial function is a sealed box with the right type and nothing inside. Lean checks that the body is well typed, compiles it so that it can run, and then keeps only the sealed box for reasoning. Even the obvious fact that the count for 1 is 0 cannot be proved by opening the box:

example : collatz 1 = 0 := by rfl

Lean replies Tactic `rfl` failed: The left-hand side, then says that collatz 1 "is not definitionally equal to the right-hand side" 0.

One condition remains. The result type of a partial function must have at least one value. Otherwise a partial function promising a value of an empty type could be used to prove a falsehood, even though it never returns anything. A definition marked unsafe drops even that safeguard, and in return no theorem may refer to it.

What the rule buys

Because of this rule, every function whose definition the logic can use is total: it has an answer for every input, and the logic may reason about that answer. The price is that the author must sometimes say why a function stops. That reason is checked like any other proof. A program that cannot be given one can still be written and run, as partial, but in proofs it stays a sealed box.

Next

• Building things from constructors: the layered values that structural recursion takes apart.
• Structural and well-founded recursion: the technical treatment of both kinds of reason.