# 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:

```
plus : Nat → Nat → Nat
plus zero m = m
plus (suc n) m = suc (plus n m)
natEq : Nat → Nat → Bool
natEq zero zero = true
natEq zero (suc m) = false
natEq (suc n) zero = false
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.

```
fib : Nat → Nat
fib zero = zero
fib (suc zero) = suc zero
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).

```
ack : Nat → Nat → Nat
ack zero m = suc m
ack (suc n) zero = ack n (suc zero)
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`

pragmaThis 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`

pragmaSwitches 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:

{-# TERMINATING #-} a : A a = a

Skipping a single definition: before first clause:

b : A {-# TERMINATING #-} b = b

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

{-# TERMINATING #-} mutual c : A c = d d : A d = c

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

mutual {-# TERMINATING #-} e : A e = f f : A f = e

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

g : A h : A g = h {-# TERMINATING #-} h = g

## References¶

Andreas Abel, Foetus – termination checker for simple functional programs