[Agda] Termination

[Conor McBride]

Hi

This is a bit of a classic. I'm sure it'll be
back, so it should probably get some space somewhere.

On 2 Jun 2008, at 11:48, Geoffrey Alan Washburn wrote:

> I've just encountered my first problem with termination.  Here is a  
> really simplified example of the problem:
>
>   Test where
>   open import Data.List
>   open import Data.Nat
>
>   data Tree : Set where
>     Leaf : ℕ -> Tree
>     Node : [ Tree ] -> Tree
>
>   inc : Tree -> Tree
>   inc (Leaf n) = Leaf (n + 1)
>   inc (Node ts) = Node (Data.List.map inc ts)
>
> Essentially, it seems that Agda cannot tell that passing inc to map  
> will be terminating.

That's right. You have to know something special
about map to see why this is ok.

> This kind of recursion is not a problem for Coq's termination  
> checker, at least as long as you've defined map properly, so is  
> there something I am just doing incorrectly here?

Coq's termination checker has a hack to allow
definitions like this. I can't remember what their
criterion is, precisely. It all seems like voodoo
to me.

>   Or is the only solution here to define a specialized version of  
> map mutually recursively with inc?

Well, that's *one* solution: it's clear that
specializing map gives rise to a mutual recursion
which satisfies the size change principle.

Fans of type-based termination would point out
that ts is a "list of *smaller* trees", and since
inc may be applied recursively to a smaller tree,
there should be no trouble with map. You can replicate
this argument without waiting for a cleverer checker
by indexing your trees with a bound on their depth.

Meanwhile, fans of structured recursion principles
will note that your inc is an instance of the
iteration operator for Tree, which should somehow (ie
by generic programming) be available for free.
Certainly, you should only need to write it once
(possibly by specializing map), and then instantiate
it.

Perhaps the deeper problem here is the structural
properties (in particular, containerhood) of lists
are not made conspicuous by their definition.
Moreover, your trees are obviously (to a human)
containers of their leaf-labels, hence operations
like inc should come for free. What we need is
language in which to make these observations
clear to the machine.

It would be amusing to compile a collection of
examples about which the Coq and Agda termination
oracles differ in opinion. But perhaps also, one
might hope to sidestep the need for oracular
approval by exposing the structural properties
upon which the explanation relies.

I'm optimistic that we can use dependent types to
describe families of computations which make sense,
rather than placing exclusive reliance on hardwired
criteria.

All the best

Conor

PS Hi to all at AIM8! I hope it's going well.