<div dir="ltr">The --no-termination-check flag will still treat functions as terminating. The motivation for the<br><div>new behaviour (which I honestly thought was the intended behaviour all along) is to let you</div><div>
write possibly non-terminating programs without jeopardising decidability of type checking.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jul 4, 2014 at 3:45 PM, Dan Licata <span dir="ltr"><<a href="mailto:drl@cs.cmu.edu" target="_blank">drl@cs.cmu.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Wait, I'm confused.<div><br></div><div>I thought from the comment that<div><br></div>
<pre style="margin-top:0px;margin-bottom:0px;padding:1em;line-height:1.1em;clear:both;background-color:rgb(249,249,249)">Note that with the pragma {-# NO_TERMINATION_CHECK #-} you can make
Agda treat any function as terminating.</pre><div><br></div><div>in the 2.4.0 release notes that NO_TERMINATION_CHECK allowed you to say "I promise this is terminating, so please treat it as such and unfold it during type checking". Is there no way to turn off the termination checker in such a way that things reduce any more? </div>
<div><span class="HOEnZb"><font color="#888888"><div><br></div><div>-Dan</div></font></span><div><br><div><div><div class="h5"><div>On Jul 4, 2014, at 5:45 AM, Ulf Norell <<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>> wrote:</div>
<br></div></div><blockquote type="cite"><div><div class="h5"><div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jul 3, 2014 at 6: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>On Thu, 2014-07-03 at 15:06 +0200, Ulf Norell wrote:<br>
> Using NO_TERMINATION_CHECK is not going to cause the type<br>
> checker to loop. What happens is that the type checker simply won't<br>
> evaluate functions that haven't been termination checked.<br>
<br>
<br>
</div>How does the below program correspond to these your two assertions?<br>
<br>
----------------------------------------------------------------------<br>
open import Foreign.Haskell<br>
open import IO.Primitive<br>
open import Data.String as String using (toCostring)<br>
open import Function using (case_of_)<br>
open import Relation.Nullary using (yes; no; ¬_)<br>
open import Relation.Unary using (Decidable)<br>
open import Relation.Binary.PropositionalEquality as PE using<br>
(_≡_; refl)<br>
open import Data.Empty using (⊥)<br>
open import Data.Product using (_,_; proj₁; Σ)<br>
open import Data.Nat using (ℕ; suc)<br>
<br>
{-# NO_TERMINATION_CHECK #-}<br>
<div>findNatByContra :<br>
(P : ℕ → Set) → (P? : Decidable P) → ¬ (∀ n → ¬ P n) → Σ ℕ P<br>
findNatByContra P P? _ = findFrom 0<br>
where<br>
findFrom : ℕ → Σ ℕ P<br>
findFrom n = case P? n of \ { (yes Pn) → (n , Pn)<br>
; (no _) → findFrom (suc n) }<br>
</div><div>False : ℕ → Set<br>
False _ = ⊥<br>
<br>
decFalse : Decidable False<br>
decFalse _ = no (λ x → x)<br>
<br>
loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False<br>
loopy H = findNatByContra False decFalse H<br>
<br>
</div><div>thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42<br>
thm _ = refl<br>
<br>
</div>main : IO Unit<br>
main = putStrLn (toCostring "done")<br>
----------------------------------------------------------------------<br>
<br>
1) The checker loops at it (Agda 2.4.0).<br>
2) If thm is removed, than it is checked and compiled.<br></blockquote><div><br></div><div>That's a bug, which I've now fixed.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
3) In expect that this NO_TERMINATION_CHECK applies only to the<br>
function findNatByContra. Right?<br></blockquote><div> </div><div>Yes.</div><div><br></div><div>/ Ulf</div><div><br></div></div></div></div></div></div><div class="">
_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">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></blockquote></div><br></div></div></div></div></blockquote></div><br></div>