partial def is the honest answer for Collatz

Idris 2 gives you a third label, and it's the one I reach for most. total is your honest def. partial is your partial def. In between sits covering. Every input has a matching clause, but termination isn't promised. For the Collatz count that's the useful claim, because the thing I actually get bitten by is a missing case, not a loop. And %default total at the top of a file flips the burden for everything else, which is handy when a module is mostly arithmetic.

For contrast, a plain OCaml arrow claims even less than covering does. The type of the same function is int -> int, and a let rec is accepted whatever it does at run time. It doesn't even promise that every pattern is handled, because a non-exhaustive match is only a warning. The smaller claim is fine, provided nobody reads the arrow as saying more than it does.

Worth separating two kinds of program here. The Collatz count should return a number, so termination is the right question. A read-eval-print loop or a server should never return, and the property you want is that each turn of the loop finishes and the loop itself runs in constant space.

Scheme gives me the second one for free. R7RS requires proper tail calls, so a server is just a procedure calling itself in tail position.

A totality checker has nothing to say about that loop, and neither does partial.

Not nothing. A Lean main loop is a partial def in IO, but the pure step it calls each turn can be total, and the checker is there for that step.

Here's the fuel version, for comparison.

def collatzFuel : Nat → Nat → Option Nat
  | 0, _ => none
  | _ + 1, 1 => some 0
  | fuel + 1, n =>
    let next := if n % 2 == 0 then n / 2 else 3 * n + 1
    (collatzFuel fuel next).map (· + 1)

#eval collatzFuel 1000 27  -- some 111
#eval collatzFuel 100 27   -- none

Lean found the structural recursion on fuel with no annotation. Total. none can only mean the fuel ran out, since every run that reaches 1 returns some.

Mind the second #eval. 100 sounds like plenty of fuel for small inputs, and 27 alone takes 111 steps.

partial def stays for running, and the fuel version is the one I can evaluate inside proofs.

The fuel version reads a lot like the timeout in my Go handoff test. The select there gives up after two seconds, the test fails, and nobody takes that as a statement about the worker, only that it didn't answer in time. Your none looks like the same kind of give-up to me, a bound picked so that the run ends somewhere.

If that's the right way to see it, maybe the fuel deserves to be as visible at the call site as 2 * time.Second is in the test, so a reader knows which number decides the outcome.

Different thing. The fuel is already visible. It is the first argument.

Your timeout sits outside the program. When it fires, the test fails and the code under test learns nothing it could use. none is a value of the function's own type. A proof can case on it. A lemma like collatzFuel f n = some k → collatzFuel (f + 1) n = some k goes through by induction on f, generalizing n. So more fuel never changes an answer that already came back.

A test that gave up has no such lemma about it.

The fuel you need is the step count plus one, since reaching 1 still costs a unit. 27 needs 112, and collatzFuel 111 27 comes back none.

SQL has the same situation in WITH RECURSIVE, and PostgreSQL does not ask whether the recursion ends. The recursive term runs until an iteration returns no rows. Drop the n <> 1 filter and the 4, 2, 1 cycle continues until something outside the query stops the statement. The usual repair is a depth column, which is your fuel under another name.

WITH RECURSIVE steps(n, depth) AS (
  SELECT 27, 0
  UNION ALL
  SELECT CASE WHEN n % 2 = 0 THEN n / 2 ELSE 3 * n + 1 END, depth + 1
  FROM steps
  WHERE n <> 1 AND depth < 1000
)
SELECT max(depth) FROM steps;

This returns 111 for 27. PostgreSQL 14 added a CYCLE clause that stops a path once a value repeats, so it would catch the forgotten filter. It cannot help with a sequence that never repeats, and there the depth cap remains the only bound. PostgreSQL also has an overflow detail here. 3 * n + 1 on integer raises an out of range error instead of wrapping, so large starts want bigint.

Same shape, with a gap. max(depth) cannot tell a finished run from a cut one when it reports exactly 1000. Lean puts that distinction in the type. The query has to select it.

Take the deepest row and return its n with the depth, ORDER BY depth DESC LIMIT 1. n = 1 maps to some depth, and any other n at the cap maps to none.