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 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:
- Constructor elimination: if cons is a constructor, x < cons a1..an x b1..bn,
- 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.