Termination Checker

The termination checker of Agda is basically the same as Foetus (ref). For example, let me consider the following function case.

  add : (x y : Nat) -> Nat
  add zero y = y
  add (suc x') y = suc (add x' y)

The mechanism checks the parameters of recursive calls. In the third line, the argument suc x', y depend on parameters x', y in the recursive call. We represent this x'< suc x', y=y by using the dependency relation. To be precise, the dependency relation is defined as follows:

  1. Constructor elimination: if cons is a constructor, x < cons a1..an x b1..bn,
  2. Application: if y<x then (ya)<x where a is a vector of terms.

In any recursive call, dependency order of x decrease, so the computation will eventually terminate.

Let's give an example. First, constructor names do not matter e.g. c1 x < c0 (c1 x). So the function foo1 passes the termination check. Let's define the following datatype.

  data Bin : Set where
  eps : Bin
  c0  : Bin -> Bin
  c1  : Bin -> Bin

  foo1 : Bin -> Nat
  foo1 eps = zero
  foo1 (c0 eps) = zero
  foo1 (c0 (c1 x)) = suc (foo1 (c0 x))
  foo1 (c0 (c0 x)) = suc (foo1 (c0 x))
  foo1 (c1 x)      = suc (foo1 x)

However, the following foo2 doesn't pass the termination check since c1 x < c0 (c0 x) does not hold.

  foo2 : Bin -> Nat
  foo2 eps = zero
  foo2 (c0 eps) = zero
  foo2 (c0 (c1 x)) = suc (foo2 (c0 x))
  foo2 (c0 (c0 x)) = suc (foo2 (c1 x))
  foo2 (c1 x)      = suc (foo2 x)

This means that size-change termination has not been implemented to Agda.

And, uncurrying also works:

  add1 : Pair Nat Nat -> Nat
  add1 (pair x (succ y)) = succ (add1 (pair x y))
  add1 (pair x zero)     = x

It is said that uncurrying makes termination checking easier. However, in Agda this is not the case. This is because the Pair datatype is not native to Agda by default.

As for the multi-argument case, sometimes the dependency relations don't match in many parameters. Let's see the Ackerman function case:

  ack : (x y : Nat) -> Nat
  ack zero n = s n
  ack (suc m) zero = ack m (suc zero)
  ack (suc m) (suc n) = ack m (ack (suc m) n)

To show ack terminates, we define a lexicographic order on parameters with respect to the dependency order as follows:

  (x,y)<<(x', y') iff (x<x' or (x<=x' & y<y'))

In any recursive call of ack, this lexicographic order decreases. We call such an order a "termination order", and we judge that ack will eventually terminate since it has a termination order.

Next, let's see the mutual definition case.

  mutual

  data Even : Set where
  zeroE : Even
  succE : Odd -> Even

  data Odd : Set where
  succO : Even -> Odd

  mutual

  addOO : Odd -> Odd -> Even
  addOO (succO x) y = succE (addEO x y)

  addEO : Even -> Odd -> Odd
  addEO zeroE y = y
  addEO (succE x) y = succO (addOO x y)

Here addOO is defined by using addEO and vice versa. In such case, first we list the all possible path of recursive call (they form graph: it is called completed call graph). In this case, addOO has only a path

 addOO -> addEO -> addOO. 

Next we try to define a lexicographic order of parameters which decrease in recursive call. Since we can define such the one lexicographic order for all possible path, these function pass the termination check.

We note that Agda's termination check is not perfect: there are mutually defined functions which Agda can not judge they will terminate.

  h : (x y : Nat) -> Nat
  h zero zero = zero
  h zero (suc y) = h zero y
  h (suc x) y = h x y

  mutual

  f : (x y : Nat) -> Nat
  f zero z = zero
  f (suc x) zero = zero
  f (suc x) (suc y) = h (g x y) (f (suc (suc x)) y)

  g : (x y : Nat) -> Nat
  g zero y = zero
  g (suc x) zero = zero
  g (suc x) (suc y) = h (f x y) (g x (suc (suc y)))

Here, h is constantly equal to zero, so both f and g must be constantly equal to zero. However, in the recursive call via the path f -> g -> g -> f, parameter's dependency order doesn't decrease.

References

  1. Andreas Abel, Foetus termination checker for simple functional programs