Termination Checking

Not all recursive functions are permitted - Agda accepts only these recursive schemas that it can mechanically prove terminating.

Primitive recursion

In the simplest case, a given argument must be exactly one constructor smaller in each recursive call. We call this scheme primitive recursion. A few correct examples:

  1. plus : Nat → Nat → Nat
  2. plus zero    m = m
  3. plus (suc n) m = suc (plus n m)
  5. natEq : Nat → Nat → Bool
  6. natEq zero    zero    = true
  7. natEq zero    (suc m) = false
  8. natEq (suc n) zero    = false
  9. natEq (suc n) (suc m) = natEq n m

Both plus and natEq are defined by primitive recursion.

The recursive call in plus is OK because n is a subexpression of suc n (so n is structurally smaller than suc n). So every time plus is recursively called the first argument is getting smaller and smaller. Since a natural number can only have a finite number of suc constructors we know that plus will always terminate.

natEq terminates for the same reason, but in this case we can say that both the first and second arguments of natEq are decreasing.

Structural recursion

Agda’s termination checker allows more definitions than just primitive recursive ones – it allows structural recursion.

This means that we require recursive calls to be on a (strict) subexpression of the argument (see fib below) - this is more general that just taking away one constructor at a time.

  1. fib : Nat → Nat
  2. fib zero          = zero
  3. fib (suc zero)    = suc zero
  4. fib (suc (suc n)) = plus (fib n) (fib (suc n))

It also means that arguments may decrease in an lexicographic order - this can be thought of as nested primitive recursion (see ack below).

  1. ack : Nat → Nat → Nat
  2. ack zero    m       = suc m
  3. ack (suc n) zero    = ack n (suc zero)
  4. ack (suc n) (suc m) = ack n (ack (suc n) m)

In ack either the first argument decreases or it stays the same and the second one decreases. This is the same as a lexicographic ordering.

With-functions

Pragmas and Options

  • The NON_TERMINATING pragma

    This is a safer version of TERMINATING which doesn’t treat the affected functions as terminating. This means that NON_TERMINATING functions do not reduce during type checking. They do reduce at run-time and when invoking C-c C-n at top-level (but not in a hole). The pragma was added in Agda 2.4.2.

  • The TERMINATING pragma

    Switches off termination checker for individual function definitions and mutual blocks and marks them as terminating. Since Agda 2.4.2.1 replaced the NO_TERMINATION_CHECK pragma.

    The pragma must precede a function definition or a mutual block. The pragma cannot be used in --safe mode.

    Examples:

    • Skipping a single definition: before type signature:

      1. {-# TERMINATING #-}
      2. a : A
      3. a = a

    • Skipping a single definition: before first clause:

      1. b : A
      2. {-# TERMINATING #-}
      3. b = b

    • Skipping an old-style mutual block: Before mutual keyword:

      1. {-# TERMINATING #-}
      2. mutual
      3.   c : A
      4.   c = d
      6.   d : A
      7.   d = c

    • Skipping an old-style mutual block: Somewhere within mutual block before a type signature or first function clause:

      1. mutual
      2.  {-# TERMINATING #-}
      3.  e : A
      4.  e = f
      6.  f : A
      7.  f = e

    • Skipping a new-style mutual block: Anywhere before a type signature or first function clause in the block:

      1. g : A
      2. h : A
      4. g = h
      5. {-# TERMINATING #-}
      6. h = g

References

Andreas Abel, Foetus – termination checker for simple functional programs