[Agda] termination by contradiction

[Ulf Norell]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140704/a4bf8b42/attachment.html