[Agda] termination by contradiction

[Ulf Norell]

I think the name fits quite well with the usual meaning of non-termination.
You just have to keep in mind that we care not only about run-time
termination, but also compile-time termination on open terms. In your case
findNatByContra is non-terminating in the presence of false assumptions. If
you have a function that is really terminating on closed as well as open
terms, then NO_TERMINATION_CHECK will work just fine.

/ Ulf


On Mon, Jul 7, 2014 at 8:15 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

> On Mon, 2014-07-07 at 21:56 +0400, Sergei Meshveliani wrote:
> > On Mon, 2014-07-07 at 18:11 +0200, Ulf Norell wrote:
> > >
> > > On Mon, Jul 7, 2014 at 2:36 PM, Sergei Meshveliani <mechvel at botik.ru>
> > > wrote:
> > >
> > >         I have installed Agda of July 7, 2014
> > >         (in which the checker loop is fixed), and tried this program
> > >         version:
> > >
> ----------------------------------------------------------------
> > >         {-# NO_TERMINATION_CHECK #-}
> > >         findNatByContra :
> > >                (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) →
> Σ ℕ P
> > >         findNatByContra P P? _ =  findFrom 0
> > >           where
> > >           findFrom : ℕ → Σ ℕ P
> > >           findFrom n = case P? n of \ { (yes Pn) → (n , Pn)
> > >                                       ; (no _)   → findFrom (suc n) }
> > > [..]
> >
> > >         I am trying to provide the feature ``classic termination
> > >         proof'' with
> > >         some possibilities in Agda.
> > > [..]
>
>
> > First of all, I got overruled on the behaviour of
> > NO_TERMINATION_CHECK. I've implemented a new pragma NON_TERMINATING
> > with the non-looping behaviour.
>
> 1) As I wrote before, the word  `non-terminating'  (algorithm Foo)
>    already has a default meaning:
>    ``Foo does not terminate at each argument'',
>    or may be,  ``Foo does not terminate at some argument''.
>
> 2) Is the word  TERMINATES  adequate?
>    (the meaning is ``postulate that it terminates'').
>
> Regards,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> 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/20140707/8dbbe5ff/attachment.html