[Agda-dev] Termination

[Pierre Hyvernat]

>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
-- 
This fortune is inoperative.  Please try another.