# Termination Checker

The information on this page is likely to be out of date. See the official user manual for the most up-to-date version of the information on this page.

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

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

addEO : Even -> Odd -> Odd
```

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