[Agda] termination by contradiction

[Ulf Norell]

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> 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> 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/2431aab4/attachment-0001.html