[Agda] On termination checkers

[Matthew Daggitt]

Hi David,
 I asked a *very* similar question in a recent issue
<https://github.com/agda/agda/issues/3842> on the Agda Github. You might be
interested in Andreas's reply.
Best,
Matthew

On Wed, Jun 12, 2019 at 7:03 PM Andrew Pitts <andrew.pitts at cl.cam.ac.uk>
wrote:

>
> > On 12 Jun 2019, at 10:09, david.janin at labri.fr wrote:
> >
> > Dear Andrew,
> >
> > To your question, what shall be the best sizing for (inductive) lists,
> > experiment seems to show that the answer is none !!!
> >
> > I describe below the arguments with examples piled one on top of the
> other,  the
> > correct code being enclosed.
> >
> > The experiment consists in trying all discussed definitions of sized
> (inductive)
> > list, dropping the pack/unpack aspects that is now irrelevant, and
> trying to prove
> > some expected (easy) list’s properties.
> >
> > The possibilities discussed so far  (given in incorrect « piled » Agda
> code) are:
> > ...
> > Or this suggests that sized type are bound to be used with co-induction
> so that
> > escape towards infinity is possible.
>
> I don’t think so. The way I see it is as follows.
>
> Sized types can be useful with inductive data when one has a recursive
> definition of a function on the data that is semantically well-defined, but
> which Agda’s termination check can't see as such. Some sized version of the
> data type (there may be several different ones!) may allow a definition of
> the recursive function to pass the checker and do the right thing “at
> infinity”. But especially for functions of several arguments there could be
> many different ways (or none!) of introducing size information in the
> arguments and results that does the job at infinity. So in your experiments
> I would say it’s not so much a question of which of the data declarations
> (SList1, SList2 or SList3) is better, as to how to introduce sizes in your
> select/unchanged/append function definitions — and that delicately depends
> upon their intended meaning — there won’t be one fixed pattern of what to
> do (and in some cases it may be impossible).
>
> Here endeth my 2p worth.
>
> Andy
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190612/4aa0e5ab/attachment.html>