[Agda] termination by contradiction

[Ulf Norell]

Using NO_TERMINATION_CHECK is not going to cause the type
checker to loop. What happens is that the type checker simply won't
evaluate functions that haven't been termination checked. So it's
perfectly safe for you to use findNatByContra in your programs. At
run-time it will run fine, but you won't be able to prove any theorems
about it since it doesn't reduce at type checking time.

/ Ulf


On Thu, Jul 3, 2014 at 2:20 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

> On Wed, 2014-07-02 at 22:55 +0200, Ulf Norell wrote:
> >
> > On Wed, Jul 2, 2014 at 7:42 PM, Sergei Meshveliani <mechvel at botik.ru>
> > wrote:
> >
> >         2) Suppose one introduces `loopy' by a mistake, and sets its
> >         various
> >         invocations, also by a mistake. What can happen then, in the
> >         worst case?
> >         Probably, the type checker will loop forever, and the user
> >         will
> >         interrupt the process of checking (as I did 10 minutes ago!).
> >         This will not make the whole usage worse, because there are
> >         many other
> >         ways in Agda to make the checker loop forever.
> >
> >
> > There shouldn't be any ways to make the type checker loop forever, so
> > if you have
> > any, please report them as bugs. There's a big difference between the
> > type checker
> > looping and there being inefficiencies in the type checker or your
> > program, making
> > checking take a very long time (or run out of memory).
> >
>
>
> I see. Thank you.
>
> As to Markov's rule for termination, I understand this as follows.
> 1) It can be used in an Agda program by postulating termination like it
> is done in  NO_TERMINATION_CHECK for  findNatByContra.
> 2) This will lead to a  non-terminated  type-check for some functions
> applying  findNatByContra
> (and I doubt on whether such functions can appear in a practical program
> other than by a mistake).
>
> Regards,
>
> ------
> Sergei
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140703/b50e7234/attachment.html