Sized Types [Re: [Agda] proving termination trouble again]

[Andreas Abel]

Robin Green a écrit :
> How do sized types compare to defining a function using well-founded
> recursion? What are the advantages and disadvantages of the two
> approaches?

Hi Robin,

Size is a reflection of the structural order that is hardwired in Agda 
into the language of types.  Using sized types, you can make Agda "see" 
more size relations, i.e. that minus m n is structurally less or equal 
than m.

The advantage is that sized types are mostly automatic, with a little 
annotation required to help the type reconstruction.

Well-founded recursion has the advantage that it is very general.  Where 
structural order and sized types fail, one can always continue with 
well-founded recursion.  However, one needs to define an order, prove 
its wellfoundedness and then add an extra argument, containing the proof 
of wellfoundedness, to the recursive function at hand.  Recursion is 
then done on the proof of wellfoundedness, an how to erase these proofs 
during compilation is an open issue.

In summary, sized types and well-founded recursion are complementary. 
Well-founded recursion is needed for non-trivial termination behavior, 
and structural ordering is needed to bootstrap (wellfounded recursion is 
just structural recursion on the proof of wellfoundedness).  Sized types 
are the proper approach to structural recursion, imho.  Unfortunately, 
there are no good implementations of sized types yet.

Cheers,
Andreas

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

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/