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

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

```{-# 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
```