Totality

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

TOC

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

Table of contents

1. Introduction
2. Importance of totality
3. Ensuring totality
   1. Type checking
   2. Coverage checking
   3. Termination checking
      1. Primitive recursion
      2. Structural recursion
   4. Strict positivity of constructors checking
   5. Guardedness checking in coinductive programs
4. Detailed information
5. References

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:

1. Type checking
2. Coverage checking
3. Termination checking
4. Strict positivity of constructors checking
5. 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 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

1. Conor McBride - First-order Unification by Structural Induction