[Agda-dev] Termination

[Andreas Abel]

Ok, makes a lot of sense.  I put it on the todo list.

   https://code.google.com/p/agda/issues/detail?id=1390

Thanks for your input!

Andreas

On 12.12.2014 10:58, Pierre Hyvernat wrote:
>
>> Yes, the termination analysis is cheap in that respect, it does not
>> see that the call sequence
>>  stop (I :: n) --> stop (I :: n)
>> is impossible.  Someone (was it Jean-Yves Moyen?) suggested a smarter
>> static call graph construction,
>>
> I don't know about Jean-Yves Moyen, but that's what I implemented for
> the termination checker of the PML language.
>
>
>> Such an analysis would be much more expensive, I guess.  The question
>> is whether it is worth the effort.
>>
> In our experience, it is not that expensive. I used the usual
> size-change termination principle (which is more expensive than Agda's
> termination checker) and added constructors. Termination checking took
> much less time than type checking. (Size-change termination being
> P-space complete, there are __very expansive__ examples, but I've never
> seen them arise in practice.)
>
>
> In my opinion, it is worth the effort. Rewriting my code so that it
> passes the termination checker isn't a nice solution, especially for
> very simple programs..
> We know the termination checker can't be complete, but we should make it
> as strong as possible. There should also be a balance between strength
> and trust in the termination checker. We don't want it to become too
> complex.
>
> In all modesty :), I think the "size-change termination + constructor
> and local increase" is quite nice, easy to implement and documented.
>   http://www.lama.univ-savoie.fr/~hyvernat/Files/basic-SCT.tar
>   http://www.lama.univ-savoie.fr/~hyvernat/Files/sct.pdf
>
> The original example works in the following form:
> -------- 8< ----------
> test Nil[_] = S[Zero[_]]
> test Cons[False[_], l] = test l
> test Cons[True[_], l] = S[test Cons[False[_],l]]
> -------- 8< ----------
> (Note that the "basic-SCT" contains only the termination checker. No
> type checking is done...)
>
>
>
>> I guess I'd need to see more convincing examples,
>>
> I don't know exactly how the current termination checker works, but
> there is a problem with checking uncurried functions.
> Uncurrying functions is easy but gets very verbose with dependent types.
> That's definitely something I'd prefer avoiding...
>
> Keeping constructors makes uncurried functions no different from curried
> functions.
>
>
>
> Pierre

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/