[Agda] termination by contradiction

[Dan Licata]

Wait, I'm confused.

I thought from the comment that

Note that with the pragma {-# NO_TERMINATION_CHECK #-} you can make
    Agda treat any function as terminating.

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?  

-Dan

On Jul 4, 2014, at 5:45 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 
> On Thu, Jul 3, 2014 at 6:15 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> On Thu, 2014-07-03 at 15:06 +0200, Ulf Norell wrote:
> > Using NO_TERMINATION_CHECK is not going to cause the type
> > checker to loop. What happens is that the type checker simply won't
> > evaluate functions that haven't been termination checked.
> 
> 
> How does the below program correspond to these your two assertions?
> 
> ----------------------------------------------------------------------
> open import Foreign.Haskell
> open import IO.Primitive
> open import Data.String as String using (toCostring)
> open import Function         using (case_of_)
> open import Relation.Nullary using (yes; no; ¬_)
> open import Relation.Unary   using (Decidable)
> open import Relation.Binary.PropositionalEquality as PE using
>                                                      (_≡_; refl)
> open import Data.Empty   using (⊥)
> open import Data.Product using (_,_; proj₁; Σ)
> open import Data.Nat     using (ℕ; suc)
> 
> {-# 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) }
> False : ℕ → Set
> False _ = ⊥
> 
> decFalse : Decidable False
> decFalse _ = no (λ x → x)
> 
> loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False
> loopy H =  findNatByContra False decFalse H
> 
> thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42
> thm _ = refl
> 
> main : IO Unit
> main = putStrLn (toCostring "done")
> ----------------------------------------------------------------------
> 
> 1) The checker loops at it  (Agda 2.4.0).
> 2) If  thm  is removed, than it is checked and compiled.
> 
> That's a bug, which I've now fixed.
>  
> 3) In expect that this NO_TERMINATION_CHECK applies only to the
>    function  findNatByContra.  Right?
>  
> Yes.
> 
> / Ulf
> 
> _______________________________________________
> 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/20140704/7b4f474d/attachment.html