[Agda] size-based termination

[Conor McBride]

Hi Ondrej

On 21 Dec 2010, at 15:30, Ondrej Rypacek wrote:

> Hi all,
>
> I have a function which terminates for size but not structural  
> reasons.

Recursive function termination is always for structural reasons.  
However,
sometimes the relevant structure is not clearly apparent in the type of
the data.

> Is there a way to turn off the termination checker for this definition
> so I can continue with the development ?

I'm sure there's a handy preamble option flag for that purpose.

> What is the best way of doing this properly ? I.e. how to turn a
> size-terminating function into a structurally recursive one ?

You may find Andreas Abel's "sized types" useful in this respect. Agda  
does
have an experimental implementation of them, doesn't it?

Alternatively, you might index your datatype by a size (or an upper  
bound
on size). If the size decreases structurally, you're sorted.

Explicit size indexing can be a nuisance without some cheap means to
inflate the bound: that's a big part of what "sized types" sort out.

It's certainly worth looking in that direction.

I see Andreas has just suggested the "gasoline" method...

All the best

Conor