<div dir="ltr">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.<div>
<br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Jul 7, 2014 at 8:15 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="">On Mon, 2014-07-07 at 21:56 +0400, Sergei Meshveliani wrote:<br>
> On Mon, 2014-07-07 at 18:11 +0200, Ulf Norell wrote:<br>
> ><br>
> > On Mon, Jul 7, 2014 at 2:36 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> > wrote:<br>
> ><br>
> > I have installed Agda of July 7, 2014<br>
> > (in which the checker loop is fixed), and tried this program<br>
> > version:<br>
> > ----------------------------------------------------------------<br>
> > {-# NO_TERMINATION_CHECK #-}<br>
> > findNatByContra :<br>
> > (P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P<br>
> > findNatByContra P P? _ = find>From 0<br>
> > where<br>
> > findFrom : ℕ → Σ ℕ P<br>
> > findFrom n = case P? n of \ { (yes Pn) → (n , Pn)<br>
> > ; (no _) → findFrom (suc n) }<br>
</div>> > [..]<br>
<div class="">><br>
> > I am trying to provide the feature ``classic termination<br>
> > proof'' with<br>
> > some possibilities in Agda.<br>
</div>> > [..]<br>
<div class=""><br>
<br>
> First of all, I got overruled on the behaviour of<br>
> NO_TERMINATION_CHECK. I've implemented a new pragma NON_TERMINATING<br>
> with the non-looping behaviour.<br>
<br>
</div>1) As I wrote before, the word `non-terminating' (algorithm Foo)<br>
<div class=""> already has a default meaning:<br>
``Foo does not terminate at each argument'',<br>
or may be, ``Foo does not terminate at some argument''.<br>
<br>
</div>2) Is the word TERMINATES adequate?<br>
(the meaning is ``postulate that it terminates'').<br>
<br>
Regards,<br>
<div class="HOEnZb"><div class="h5"><br>
------<br>
Sergei<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>