**See the official user manual for the most up-to-date version of the information on this page.**

This document has been extracted from a literate Agda file, which was tested with Agda 2.3.0

## Table of contents

## Introduction

Agda is a **total** language, so all computations must terminate and return a value without any run-time errors.
This means that effectively not all programs that can be defined in (for instance) Haskell or ML can defined in Agda.
We also say that in a total language all computations are **strongly-normalizing**.

## Importance of totality

Knowing that your programs will always evaluate successfully is a nice thing to have by itself, but there is a deeper reason.

In a dependently typed language, computations may be required not only at run-time, but also during type checking. If arbitrary (i.e. non-terminating) computations were allowed, then the typechecking would become undecidable - the type checker would loop from time to time.

**Examples**. Suppose that `foo : Bool`

and evaluation of `foo`

never ends.
This program would loop the type checker (`_==_`

is the usual propositional equality):

fooIsTrue : foo == true fooIsTrue = refl

Another example:

getType : Bool -> Set getType true = Nat getType false = Bool nat? : getType foo nat? = 5

We need to check if `getType foo == Nat`

, but to do that we need to fully evaluate `foo`

- but we assumed that this would never end.

## Ensuring totality

To make sure that all computations are total, a few checks are performed in Agda:

- Type checking
- Coverage checking
- Termination checking
- Strict positivity of constructors checking
- Guardedness checking in coinductive programs

The first 3 positions are the most essential ones, the rest can be skipped on first reading.

### Type checking

Type checking rules out run-time errors like applying a function that expects a `Nat`

to a `Bool`

.

### Coverage checking

Coverage checking rules out partial functions - i.e. functions defined by pattern matching with some cases omitted.

For example, if this was allowed

data Color : Set where Red Green Blue : Color flipColor : Color -> Color flipColor Red = Green flipColor Green = Red -- no pattern for Blue

then evaluating `flipColor Blue`

would result in a run-time error.

(Agda rejects this definition with "Incomplete pattern matching for flipColor".)

Therefore, **when defining a function by pattern matching in Agda one must cover all cases**
(more precisely, all cases that are correct with respect to types).

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

data Nat : Set where zero : Nat suc : Nat -> Nat 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 rec. 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

In some systems (i.e. Coq) primitive recursion is the only allowed scheme. Agda's termination checker is less restrictive - 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.

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

below).

**Example** (Fibonacci's numbers):

fib : Nat -> Nat fib zero = zero fib (suc zero) = suc zero fib (suc (suc n)) = plus (fib n) (fib (suc n))

**Example** (Ackermann's function)

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.

### Strict positivity of constructors checking

See the section about strict-positivity from Simple Inductive Types.

### Guardedness checking in coinductive programs

See the page for (Guarded) Coinduction.

## Detailed information

Termination Checker - algorithm details

## References

- Conor McBride - First-order Unification by Structural Induction