Termination Proofs

A function is total if it always returns a value — no infinite loops, no infinite recursion. Deppy can prove termination for recursive functions using well-founded ordering: you identify a quantity that strictly decreases on every recursive call and is bounded below (typically by zero). This is essential for using functions inside proofs — a non-terminating function could "prove" anything, because its return type is vacuously inhabited.

Why Termination Matters

In ordinary Python, a function that loops forever simply hangs or eventually crashes with RecursionError. That's annoying, but it's a runtime problem. In a proof system the stakes are higher:

Total functions are safe. They always produce a result of the declared return type.
Non-terminating functions break logic. If a function never returns, it can inhabit any type — including False. That makes the entire proof system unsound.
Deppy defaults to checking termination for every recursive function it verifies. If it cannot establish termination automatically, it asks you for a decreasing measure.
Python itself doesn't check termination. RecursionError is a safety net, not a proof. Deppy's analysis is purely mathematical.

Structural Recursion (Automatic)

When a recursive call operates on a strict substructure of an argument, termination is obvious and Deppy detects it without any annotation. Two classic patterns:

Natural-number recursion

def factorial(n: int) -> int:
    # n decreases by 1 on every recursive call
    if n <= 0:
        return 1
    return n * factorial(n - 1)

List recursion

def sum_list(xs: list[int]) -> int:
    # xs[1:] is strictly shorter than xs
    if not xs:
        return 0
    return xs[0] + sum_list(xs[1:])

Verification output for both:

$ python -m deppy.pipeline.run_verify examples/factorial.py
  ✓ factorial: structural recursion detected (n ↦ n−1)
  ✓ termination: Z3_VERIFIED

$ python -m deppy.pipeline.run_verify examples/sum_list.py
  ✓ sum_list: structural recursion detected (xs ↦ xs[1:])
  ✓ termination: Z3_VERIFIED

Tip. Start with simple structural recursion whenever possible. If your function recurses on n - 1, xs[1:], or node.left / node.right, Deppy handles it automatically — no annotations needed.

Well-Founded Recursion with `@decreases`

When the recursive structure isn't immediately obvious, you annotate the function with @decreases(expression). The expression must evaluate to a natural number (≥ 0) and must strictly decrease on every recursive call.

Example: Greatest Common Divisor

In gcd(a, b), the recursive call is gcd(b, a % b). The second argument decreases because a % b < b whenever b > 0.

from deppy import decreases

@decreases(lambda a, b: b)
def gcd(a: int, b: int) -> int:
    if b == 0:
        return a
    return gcd(b, a % b)

$ python -m deppy.pipeline.run_verify examples/gcd.py
  ✓ gcd: @decreases(b) — Z3 proved a % b < b for b > 0
  ✓ termination: Z3_VERIFIED

Example: Binary Search

The search range hi - lo shrinks on every call, reaching zero when the element is found or the range is empty.

from deppy import decreases

@decreases(lambda xs, target, lo, hi: hi - lo)
def binary_search(
    xs: list[int],
    target: int,
    lo: int = 0,
    hi: int | None = None,
) -> int | None:
    if hi is None:
        hi = len(xs)
    if lo >= hi:
        return None
    mid = (lo + hi) // 2
    if xs[mid] == target:
        return mid
    elif xs[mid] < target:
        return binary_search(xs, target, mid + 1, hi)
    else:
        return binary_search(xs, target, lo, mid)

$ python -m deppy.pipeline.run_verify examples/binary_search.py
  ✓ binary_search: @decreases(hi - lo)
    — branch xs[mid] < target: hi−(mid+1) < hi−lo  ✓
    — branch xs[mid] > target: mid−lo < hi−lo      ✓
  ✓ termination: Z3_VERIFIED

Lexicographic Ordering

Some functions need a tuple measure. Deppy uses lexicographic ordering: the first component must decrease, or it stays the same and the second component decreases, and so on. Pass multiple arguments to @decreases to specify a tuple.

Example: Ackermann Function

The Ackermann function is a classic test case for termination checkers. It grows faster than any primitive-recursive function, but it does terminate — witnessed by the lexicographic order (m, n).

from deppy import decreases

@decreases(lambda m, n: (m, n))
def ackermann(m: int, n: int) -> int:
    if m == 0:
        return n + 1
    elif n == 0:
        return ackermann(m - 1, 1)
    else:
        return ackermann(m - 1, ackermann(m, n - 1))

$ python -m deppy.pipeline.run_verify examples/ackermann.py
  ✓ ackermann: @decreases(m, n) — lexicographic
    — branch m=0:            base case                       ✓
    — branch n=0:            (m−1, 1)   <_lex (m, 0)        ✓
    — branch else (inner):   (m, n−1)   <_lex (m, n)        ✓
    — branch else (outer):   (m−1, _)   <_lex (m, n)        ✓
  ✓ termination: Z3_VERIFIED

Fuel-Based Termination

Sometimes you cannot prove that a function terminates — either because it's an open conjecture or because the proof is beyond Z3's reach. In these cases you can supply a fuel budget: Deppy will verify correctness assuming the function finishes within that many recursive calls.

from deppy import fuel

@fuel(1000)
def collatz(n: int) -> int:
    """Return the number of steps to reach 1."""
    if n == 1:
        return 0
    elif n % 2 == 0:
        return 1 + collatz(n // 2)
    else:
        return 1 + collatz(3 * n + 1)

$ python -m deppy.pipeline.run_verify examples/collatz.py
  ⚠ collatz: termination not proven — using fuel budget (1000)
  ✓ per-step correctness: Z3_VERIFIED
  ◐ termination: FUEL_BOUNDED (trust level reduced)

The verification level for fuel-bounded functions is FUEL_BOUNDED, which is weaker than Z3_VERIFIED. Other functions that depend on a fuel-bounded function inherit the reduced trust level.

While Loops and Termination

Recursive functions aren't the only source of non-termination. A while loop can also run forever. Deppy handles this with @loop_variant: you specify an expression that decreases on every iteration and is bounded below by zero.

Example: Integer Division by Repeated Subtraction

from deppy import loop_variant, guarantee

@guarantee("returns (quotient, remainder) such that a == b * q + r and 0 <= r < b")
def divmod_sub(a: int, b: int) -> tuple[int, int]:
    assert a >= 0 and b > 0
    q = 0
    r = a

    @loop_variant(lambda: r)   # r decreases each iteration
    while r >= b:
        r = r - b
        q = q + 1

    return (q, r)

$ python -m deppy.pipeline.run_verify examples/divmod_sub.py
  ✓ divmod_sub: while loop variant r
    — r decreases: r − b < r when b > 0    ✓
    — r bounded below: r ≥ 0                ✓
  ✓ guarantee: a == b * q + r ∧ 0 ≤ r < b  ✓
  ✓ termination: Z3_VERIFIED

Mutual Recursion

When two or more functions call each other, Deppy verifies a combined measure across the call graph. Each function gets its own @decreases, and Deppy checks that the measure decreases on every cross-function call.

Example: `is_even` / `is_odd`

from deppy import decreases

@decreases(lambda n: n)
def is_even(n: int) -> bool:
    if n == 0:
        return True
    return is_odd(n - 1)

@decreases(lambda n: n)
def is_odd(n: int) -> bool:
    if n == 0:
        return False
    return is_even(n - 1)

$ python -m deppy.pipeline.run_verify examples/even_odd.py
  ✓ mutual recursion group: {is_even, is_odd}
    — is_even → is_odd(n−1): n−1 < n  ✓
    — is_odd → is_even(n−1): n−1 < n  ✓
  ✓ termination: Z3_VERIFIED

The `@may_diverge` Escape Hatch

If you genuinely need a function that might not terminate — for example, a REPL loop or an event listener — mark it with @may_diverge. Deppy will skip the termination check but will not allow the function's result to be used in proofs.

from deppy import may_diverge

@may_diverge
def repl() -> None:
    while True:
        line = input("> ")
        if line == "quit":
            break
        print(eval_expr(parse(line)))

Warning. Use @may_diverge sparingly. A may-diverge function cannot appear in proof terms, guarantee annotations, or lemma bodies. It weakens the verification guarantees of anything that depends on it. Reserve it for I/O loops and top-level entry points where non-termination is intentional.

Comparison with F*

Deppy's termination checking is modelled on F*'s approach:

F*	Deppy
`decreases x`	`@decreases(lambda …: x)`
`decreases (x, y)`	`@decreases(lambda …: (x, y))` — lexicographic
`Tot` effect	`@total` (default)
`Div` effect	`@may_diverge`

The key difference: F* requires you to write F* code. Deppy verifies your existing Python without modification.

Note — Python's recursion limit vs mathematical termination. Python's default recursion limit is 1000 stack frames (sys.getrecursionlimit()). This is a practical safety limit, not a mathematical one. Deppy's termination analysis is purely logical: it proves that the recursion eventually stops, regardless of how deep it goes. A function can be mathematically total but still hit Python's recursion limit for large inputs — that's an implementation concern, not a correctness concern. Use sys.setrecursionlimit() or rewrite as iteration if needed at runtime.

Putting It All Together

Here's a complete example combining @decreases, @guarantee, and structural reasoning: a verified power function with fast exponentiation.

from deppy import decreases, guarantee

@guarantee("returns base ** exp")
@decreases(lambda base, exp: exp)
def fast_pow(base: int, exp: int) -> int:
    assert exp >= 0
    if exp == 0:
        return 1
    elif exp % 2 == 0:
        half = fast_pow(base, exp // 2)
        return half * half
    else:
        return base * fast_pow(base, exp - 1)

$ python -m deppy.pipeline.run_verify examples/fast_pow.py
  ✓ fast_pow: @decreases(exp)
    — branch exp even: exp // 2 < exp   ✓
    — branch exp odd:  exp − 1 < exp    ✓
  ✓ guarantee: base ** exp               ✓
  ✓ termination: Z3_VERIFIED

Exercise — Verified Merge Sort

Write a merge_sort function that sorts a list of integers. Annotate it with @decreases to prove termination via the decreasing length of the input list.

You'll need two functions:

merge(xs, ys) — merge two sorted lists (terminates by len(xs) + len(ys)).
merge_sort(xs) — split, recurse, merge (terminates by len(xs)).

Hints:

The base case is len(xs) <= 1.
Split at mid = len(xs) // 2.
Each half is strictly shorter than xs when len(xs) >= 2.
Add @guarantee("returns a sorted permutation of xs") for full verification.

Solution:

from deppy import decreases, guarantee

@decreases(lambda xs, ys: len(xs) + len(ys))
def merge(xs: list[int], ys: list[int]) -> list[int]:
    if not xs:
        return ys
    if not ys:
        return xs
    if xs[0] <= ys[0]:
        return [xs[0]] + merge(xs[1:], ys)
    else:
        return [ys[0]] + merge(xs, ys[1:])

@guarantee("returns a sorted permutation of xs")
@decreases(lambda xs: len(xs))
def merge_sort(xs: list[int]) -> list[int]:
    if len(xs) <= 1:
        return xs
    mid = len(xs) // 2
    left = merge_sort(xs[:mid])
    right = merge_sort(xs[mid:])
    return merge(left, right)

$ python -m deppy.pipeline.run_verify examples/merge_sort.py
  ✓ merge: @decreases(len(xs) + len(ys))
    — branch xs[0] ≤ ys[0]: len(xs[1:])+len(ys) < len(xs)+len(ys)  ✓
    — branch xs[0] > ys[0]: len(xs)+len(ys[1:]) < len(xs)+len(ys)  ✓
  ✓ merge_sort: @decreases(len(xs))
    — len(xs[:mid]) < len(xs)  when len(xs) ≥ 2   ✓
    — len(xs[mid:]) < len(xs)  when len(xs) ≥ 2   ✓
  ✓ guarantee: sorted permutation                  ✓
  ✓ termination: Z3_VERIFIED

Termination Proofs

Why Termination Matters

Structural Recursion (Automatic)

Natural-number recursion

List recursion

Well-Founded Recursion with @decreases

Example: Greatest Common Divisor

Example: Binary Search

Lexicographic Ordering

Example: Ackermann Function

Fuel-Based Termination

While Loops and Termination

Example: Integer Division by Repeated Subtraction

Mutual Recursion

Example: is_even / is_odd

The @may_diverge Escape Hatch

Comparison with F*

Putting It All Together

Well-Founded Recursion with `@decreases`

Example: `is_even` / `is_odd`

The `@may_diverge` Escape Hatch