<div dir="ltr">Using NO_TERMINATION_CHECK is not going to cause the type<div>checker to loop. What happens is that the type checker simply won't</div><div>evaluate functions that haven't been termination checked. So it's</div>
<div>perfectly safe for you to use findNatByContra in your programs. At</div><div>run-time it will run fine, but you won't be able to prove any theorems</div><div>about it since it doesn't reduce at type checking time.</div>
<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Jul 3, 2014 at 2:20 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="HOEnZb"><div class="h5">On Wed, 2014-07-02 at 22:55 +0200, Ulf Norell wrote:<br>
><br>
> On Wed, Jul 2, 2014 at 7:42 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> wrote:<br>
><br>
> 2) Suppose one introduces `loopy' by a mistake, and sets its<br>
> various<br>
> invocations, also by a mistake. What can happen then, in the<br>
> worst case?<br>
> Probably, the type checker will loop forever, and the user<br>
> will<br>
> interrupt the process of checking (as I did 10 minutes ago!).<br>
> This will not make the whole usage worse, because there are<br>
> many other<br>
> ways in Agda to make the checker loop forever.<br>
><br>
><br>
> There shouldn't be any ways to make the type checker loop forever, so<br>
> if you have<br>
> any, please report them as bugs. There's a big difference between the<br>
> type checker<br>
> looping and there being inefficiencies in the type checker or your<br>
> program, making<br>
> checking take a very long time (or run out of memory).<br>
><br>
<br>
<br>
</div></div>I see. Thank you.<br>
<br>
As to Markov's rule for termination, I understand this as follows.<br>
1) It can be used in an Agda program by postulating termination like it<br>
is done in NO_TERMINATION_CHECK for findNatByContra.<br>
2) This will lead to a non-terminated type-check for some functions<br>
applying findNatByContra<br>
(and I doubt on whether such functions can appear in a practical program<br>
other than by a mistake).<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
</blockquote></div><br></div>