[Agda] termination by contradiction

[Andreas Abel]

Objection, Ulf.

NO_TERMINATION_CHECK is --no-termination-check, but for single 
definitions only.  The semantics should stay as is.

If you want to declare a definition as non-terminating, please add a new 
pragma, like

   {-# NON_TERMINATING bla #-}

which informs Agda to not unfold bla.

Cheers,
Andreas

On 04.07.2014 20:12, Ulf Norell wrote:
> The --no-termination-check flag will still treat functions as
> terminating. The motivation for the
> new behaviour (which I honestly thought was the intended behaviour all
> along) is to let you
> write possibly non-terminating programs without jeopardising
> decidability of type checking.
>
> / Ulf
>
>
> On Fri, Jul 4, 2014 at 3:45 PM, Dan Licata <drl at cs.cmu.edu
> <mailto:drl at cs.cmu.edu>> wrote:
>
>     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
>     <mailto:ulf.norell at gmail.com>> wrote:
>
>>
>>     On Thu, Jul 3, 2014 at 6:15 PM, Sergei Meshveliani
>>     <mechvel at botik.ru <mailto: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 <mailto:Agda at lists.chalmers.se>
>>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/