[Agda] termination by contradiction

[Ulf Norell]

Using abstract doesn't work for a couple of reasons. One is that abstract
is a module-wide construct, so things declared abstract will still unfold
in the defining module. But, more importantly, as I explained above, I want
a no termination check that is safe (that could at some point be allowed
with --safe). Using the incredibly unsafe NO_TERMINATION_CHECK together
with an abstract block doesn't fit that.

/ Ulf


On Mon, Jul 7, 2014 at 11:40 AM, Nicolas Pouillard <np at nicolaspouillard.fr>
wrote:

> Quoting Ulf Norell (2014-07-07 06:16:19)
> > On Fri, Jul 4, 2014 at 8:26 PM, Andreas Abel <andreas.abel at ifi.lmu.de>
> > wrote:
> >
> > > Objection, Ulf.
> > >
> > > NO_TERMINATION_CHECK is --no-termination-check, but for single
> definitions
> > > only.  The semantics should stay as is.
> > >
> > > If you want to declare a definition as non-terminating, please add a
> new
> > > pragma, like
> > >
> > >   {-# NON_TERMINATING bla #-}
> > >
> > > which informs Agda to not unfold bla.
> > >
> >
> > Ok, fine. I guess we can have both. I do think that my version is more
> > important to have though. Disabling the termination checker and treating
> > definitions as terminating anyway is a hack that shouldn't be encouraged.
> > My version can be used safely (and soundly if paired with and
> inhabitation
> > check).
>
> I'm standing with Andreas on the semantics for NO_TERMINATION_CHECK to be
> the
> same as --no-termination-check local to some definitions.
>
> Then as of having two pragmas it then raises the question whether there
> should
> be a NON_TERMINATING pragma or something to be used together with
> NO_TERMINATION_CHECK to tell Agda to not unfold. Then as mentioned
> abstract is
> here for that.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140707/e3714662/attachment.html