Posted on 2018-08-29
by Oleg Grenrus
agda

I'm positively surprised about Agda's termination checker. I'm working on a larger exercise, and Agda believes my main lemma (which does all the work for one liner theorem) terminates. But I don't, yet.

(Also there is a recent thread in /r/haskell)

I asked about Agda's termination checker on `#agda`

IRC channel, and user `gallais`

kindly responded that there's a paper from 20 years ago: * foetus - Termination Checker for Simple Functional Programs* by Andreas Abel http://www2.tcs.ifi.lmu.de/~abel/foetus.pdf.

Also, in the same discussion, `gallais`

mentioned a "hidden" Agda feature: fine grained reporting. We can specify different verbosity levels for special prefixes (parts of compiler), e.g.

`agda -v term:5 Example.agda`

As advised, you can find various reporting prefixes by grepping Agda's source code for `reportS`

.

Let's try it out:

This is very simple example, which should work in any language with termination checker.

```
open import Data.Bool
open import Data.Nat
open import Data.List
braid₁ : {A : Set} → List A → List A → List A
braid₁ [] [] = []
braid₁ [] ys = ys
braid₁ xs [] = xs
braid₁ (x ∷ xs) (y ∷ ys) = x ∷ y ∷ braid₁ xs ys
```

And Agda tells us:

```
termination checking body of braid₁
: {A : Set} → List A → List A → List A
kept call from Example.braid₁ A (_∷_ x xs) (_∷_ y ys)
to Example.braid₁ (A) (xs) (ys)
call matrix (with guardedness):
= ? ? ?
? = ? ?
? ? -1 ?
? ? ? -1
[Example.braid₁] does termination check
```

The `A`

argument stays the same `=`

, but **both** list argument decrease by one. That is stronger condition than needed for termination, but it's nice Agda finds it. There seems to be an extra dimension in the matrix, I don't know what it is :(

Agda is in fact very smart, if we rewrite the function as:

```
braid₂ : {A : Set} → List A → List A → List A
braid₂ [] ys = ys
braid₂ (x ∷ xs) ys = x ∷ braid₂ ys xs
```

Agda still thinks it terminates with:

```
termination checking body of braid₂
: {A : Set} → List A → List A → List A
kept call from Example.braid₂ A (_∷_ x xs) ys
to Example.braid₂ (A) (ys) (xs)
call matrix (with guardedness):
= ? ? ?
? = ? ?
? ? ? =
? ? -1 ?
[Example.braid₂] does termination check
```

Somehow Agda figures out an order for arguments. With higher verbosity level, it prints:

```
Idempotent call matrices (no dot patterns):
--> Example.braid₂ -->
= ? ? ?
? = ? ?
? ? -1 ?
? ? ? -1
```

i.e the same matrix as for `braid₁`

!

I'd like if Agda printed the ordering it decides from these matrices. In this example it's trivial, in others it may be less. Maybe that's something to contribute.

Next example, also mentioned in the paper, is merge from merge-sort. This is interesting example also. If I remember right, that's where Coq makes programmers do tricks.

```
merge-ord : {A : Set} → (A → A → Bool) → List A → List A → List A
merge-ord _ [] [] = []
merge-ord _ [] ys = ys
merge-ord _ xs [] = xs
merge-ord le xs@(x ∷ xs′) ys@(y ∷ ys′) with le x y
... | true = x ∷ merge-ord le xs′ ys
... | false = y ∷ merge-ord le xs ys′
```

And Agda tells us

```
termination checking body of merge-ord
: {A : Set} → (A → A → Bool) → List A → List A → List A
kept call from Example.merge-ord A le (_∷_ x xs′) (_∷_ y ys′) (true)
to Example.merge-ord (A) (le) (xs′) (y ∷ ys′)
call matrix (with guardedness):
= ? ? ? ? ?
? = ? ? ? ?
? ? = ? ? ?
? ? ? -1 ? ?
? ? ? ? = ?
kept call from Example.merge-ord A le (_∷_ x xs′) (_∷_ y ys′) (false)
to Example.merge-ord (A) (le) (x ∷ xs′) (ys′)
call matrix (with guardedness):
= ? ? ? ? ?
? = ? ? ? ?
? ? = ? ? ?
? ? ? = ? ?
? ? ? ? -1 ?
termination checking body of .Example.with-40
: {A : Set} (le : A → A → Bool) (x y : A) →
Bool → (xs′ ys′ : List A) → List A
...
======================================================================
========================= New call matrices ==========================
======================================================================
Idempotent call matrices (no dot patterns):
= ? ? ? ? ?
? = ? ? ? ?
? ? = ? ? ?
? ? ? -1 ? ?
? ? ? ? = ?
= ? ? ? ? ?
? = ? ? ? ?
? ? = ? ? ?
? ? ? = ? ?
? ? ? ? -1 ?
[Example.merge-ord] does termination check
```

Agda doesn't tell use the lexical ordering (as `foetus`

does), but it's some what visible from the matrices above.

The last example is which made me wonder how Agda's termination checker really work. Note: the calls are **nested**.

```
data Tree (A : Set) : Set where
leaf : Tree A
bin : Tree A → Tree A → Tree A
contrived : {A : Set} → Tree A → Tree A → Tree A
contrived x leaf = x
contrived x (bin y z) = contrived (contrived x y) z
```

And Agda tells us

```
termination checking body of contrived
: {A : Set} → Tree A → Tree A → Tree A
kept call from Example.contrived A x (bin y z)
to Example.contrived (A) (x) (y)
call matrix (with guardedness):
? ? ? ?
? = ? ?
? ? = ?
? ? ? -1
kept call from Example.contrived A x (bin y z)
to Example.contrived (A) (contrived x y) (z)
call matrix (with guardedness):
= ? ? ?
? = ? ?
? ? ? ?
? ? ? -1
...
======================================================================
========================= New call matrices ==========================
======================================================================
Idempotent call matrices (no dot patterns):
--> Example.contrived -->
? ? ? ?
? = ? ?
? ? ? ?
? ? ? -1
[Example.contrived] does termination check
```

The inner call is `= -1`

: `y`

is smaller than `bin y z`

. The outer call is `? -1`

: `z`

is smaller than `bin y z`

. So in both cases the last argument is decreasing one!

I wrote the program, and hadn't any idea why it terminates. Agda tells me. It feels obvious afterwards, I feel silly.

A very similar function

```
contrived₂ : {A : Set} → Tree A → Tree A → Tree A
contrived₂ x leaf = x
contrived₂ x (bin y z) = contrived₂ z (contrived₂ x y)
```

fails

```
======================================================================
========================= New call matrices ==========================
======================================================================
Idempotent call matrices (dot patterns):
--> Example.contrived₂ --> Example.contrived₂ -->
? ? ? ?
? = ? ?
? ? ? ?
? ? ? ?
```

Agda doesn't know it would terminate. I think it is bogus too, so it is good that Agda doesn't accept that function.

I still don't understand all the details of Agda's termination checker, but I see it considers all the arguments in the decision. That's very useful.

You can imagine how this matrix-business extends naturally to mutually recursive functions (no different than last example!), or to sized types (where programmer may remove some question marks!)

Site proudly generated by Hakyll