Partial definitions in proofs

The rule: #[partial] exempts executable code from the termination check. It cannot exempt a proof. A theorem — its statement or its proof term — may not reach a #[partial] definition, directly or through any chain of calls, and the compiler refuses one that does with E0063.

What the compiler refuses

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

// == a theorem may not reach a #[partial] constant, even through a wrapper
type Lst = Nil | Cons(Nat, Lst)

#[partial]
fn spin(l: Lst) -> Nat { spin(l) }

fn wrapper(l: Lst) -> Nat { spin(l) }

theorem wrapped(l: Lst): Nat { wrapper(l) }

fn main() -> Nat { 0 }

albite check wrapped.tg prints:

[E0063] Error: `wrapped` is a proof, so it may not depend on the partial constant `spin`
   ╭─[wrapped.tg:9:1]
   │
 9 │ theorem wrapped(l: Lst): Nat { wrapper(l) }
   │ ─────────────────────┬─────────────────────  
   │                      ╰─────────────────────── 
   │ 
   │ Help: a proof may not depend on a partial definition — prove the recursion terminates, or state the theorem about a total one
   │ 
   │ Note: reaches `spin` (marked `#[partial]`) through wrapper
───╯

wrapper itself is fine — it is ordinary executable code, and calling a partial function from executable code is always allowed. The error is on the theorem, and the Note: line names the chain it travelled.

What it means

albite explain error E0063 says:

#[partial] buys executable code an exemption from termination checking. It cannot buy a proof one: a proof that may reference a possibly-diverging constant proves nothing.

The restriction is transitive, which is the point. A wrapper that merely calls a partial function is itself partial, so routing a theorem through one more layer does not launder it. The message names the chain it travelled.

A definition’s type counts as well as its body — an equality statement embeds terms, so a theorem can reach a partial constant without its proof term mentioning one.

The fix is to prove the recursion terminates (rewrite it structurally, or name the decreasing parameter), or to state the theorem about a definition that is already total. Executable code is unaffected: a partial constant is welcome anywhere outside a proof.

What to write instead

Keep the partial function where it belongs — in code that runs — and state the theorem about a total one. This is tests/golden/check/docs_partial_in_proofs.tg:

// Rejected: a theorem that reaches a `#[partial]` function.
// Accepted: the theorem is about a total function; the partial one
// stays in executable code, where it is welcome.
type Lst = Nil | Cons(Nat, Lst)

#[partial]
fn digits(n: Nat) -> Nat { if n < 10 { 1 } else { 1 + digits(n / 10) } }

fn length(l: Lst) -> Nat { match l { Nil => 0, Cons(h, t) => 1 + length(t) } }

theorem measured(l: Lst): Nat { length(l) }

fn main() -> Nat { digits(length(Cons(1, Nil)) * 100) }

albite run prints 3.

When the function you want to reason about is the partial one, the only way through is to make it total: rewrite the recursion on a structural subterm, or name the decreasing parameter with #[decreasing(arg)]. See Recursion the compiler can see ends.

Ask the compiler

albite explain error E0063
albite doctor check type termination <file>

The census lists every definition’s termination verdict, including which ones are partial and which are partial only because they call one.