Recursion the compiler can see ends

The rule: a recursive function is accepted only when some parameter gets strictly smaller at every recursive call — smaller in the sense of being a piece taken out of the value by a match, not a number computed from it. Anything else is refused with E0062.

This is the rule a first recursive function is most likely to meet.

What the compiler refuses

This is the golden test tests/golden/error/docs_termination_nat_counter.tg:

// A first recursive function over a `Nat` counter. `n - 1` is a number
// computed from `n`, not a piece of it, so the compiler cannot see the
// recursion stop and refuses it (E0062).
fn count(n: Nat) -> Nat { if n == 0 { 0 } else { 1 + count(n - 1) } }

fn main() -> Nat { count(3) }

albite check count.tg prints:

[E0062] Error: cannot prove termination of `count`
   ╭─[count.tg:4:1]
   │
 4 │ fn count(n: Nat) -> Nat { if n == 0 { 0 } else { 1 + count(n - 1) } }
   │ ──────────────────────────────────┬──────────────────────────────────  
   │                                   ╰──────────────────────────────────── 
   │ 
   │ Help: rewrite the recursion structurally, or mark the definition `#[partial]` (partial definitions cannot be used in proofs)
   │ 
   │ Note: no parameter has an inductive type to descend on: `n: Nat` (a primitive — it has no subterms, so a loop over it is a measure, not a descent)
───╯

The Note: line is the key. Nat is a primitive — a machine integer — so it has no pieces for a match to take out, and n - 1 is arithmetic. Matching n against 0 does not change that: it tests the value, it does not take it apart.

What it means

albite explain error E0062 says:

A non-terminating function inhabits every type, including the empty one, so a recursive definition is admitted only once the compiler can see that it stops. Phase 1 checks the structural rule: some parameter must get strictly smaller at every recursive call.

“Strictly smaller” means bound by taking a value apart, not built back up. Matching l against Cons(h, t) proves t smaller than l; Cons(0, t) is not smaller than l, even though t is. Aliases and projections of a smaller value stay smaller; rebinding the name loses the fact.

[…]

When more than one parameter decreases at every call, the compiler will not guess: write #[decreasing(arg)]. When the recursion genuinely is not structural — an accumulator, a measure, a division — Phase 1 cannot certify it. Mark it #[partial] and it is admitted as an opaque constant that proofs may not use (see PartialInProof).

(Abridged: two paragraphs on mutual recursion and on recursion through a value are omitted — albite explain error E0062 prints them in full.)

What to write instead

There are three answers, and this is all of them in one file — tests/golden/check/docs_termination.tg:

type List = Nil | Cons(Nat, List)

// (a) Recurse on a piece of the value you took apart.
fn length(l: List) -> Nat {
    match l { Nil => 0, Cons(h, t) => 1 + length(t) }
}

// (a) Over a `Nat`, which has no pieces, use `natrec`.
fn count(n: Nat) -> Nat {
    natrec(Nat, 0, fn(k: Nat, acc: Nat) => acc + 1, n)
}

// (b) Both lists shrink at every call, so say which one to measure.
#[decreasing(a)]
fn zip_sum(a: List, b: List) -> Nat {
    match a {
        Nil => 0,
        Cons(x, rest_a) => match b {
            Nil => 0,
            Cons(y, rest_b) => x + y + zip_sum(rest_a, rest_b),
        },
    }
}

// (c) Division is a measure, not a descent: opt out.
#[partial]
fn digits(n: Nat) -> Nat {
    if n < 10 { 1 } else { 1 + digits(n / 10) }
}

fn main() -> Nat {
    length(Cons(1, Cons(2, Nil))) + count(3) + zip_sum(Cons(1, Nil), Cons(2, Nil)) + digits(1234)
}

albite run prints 12.

(a) Restructure to a subterm

If the data has a shape — a list, a tree, a user-defined type — recurse on the piece a match hands you, as length does with t. For a count over a Nat, natrec(type, base, step, n) is the structural form: it runs step n times, and the compiler knows it stops. See Induction over naturals.

(b) #[decreasing(arg)] — name the parameter

When two parameters shrink at every call, the compiler refuses to guess which one is the measure. Without the annotation, zip_sum is refused with Help: annotate the intended parameter, e.g. #[decreasing(a)]. The annotation does not weaken the check: the named parameter still has to shrink.

(c) #[partial] — the ordinary outcome for executable code

Plenty of real recursion is not structural: halving, digit loops, a cursor moving through a string, a search that stops when it finds something. Mark such a function #[partial] and the compiler accepts it without a proof that it stops.

This is not a defeat and not a hack. The Albite compiler’s own source uses #[partial] over a thousand times. What it costs is exactly one thing: a #[partial] function — and anything that calls one — may not appear in a theorem statement or a proof. See Partial definitions in proofs.

Turning the check down while you work

--termination <level> on check, run, test and compile (or the ALBITE_TERMINATION environment variable) sets how hard the check is enforced:

These exist for bisecting and for exploring, not as the normal way to build: a warning left behind is a function a later proof cannot use, and #[partial] says so in the source where the next reader will see it.

Ask the compiler

albite explain error E0062
albite info def <name> <file> --why-not-certified
albite doctor check type termination <file>

--why-not-certified says, for one definition, why each parameter was refused as the decreasing one. doctor check type termination is the census for a whole file, and it runs even on a file the check rejects.