[Agda] termination by contradiction

[Dmytro Starosud]

Nice :)

I think making "findNatByContra" primitive may help. Or not?
Anyway, "loopy" is weakness of this particular implementation of MP, but
not of MP itself.
(if I am not confused completely)

Dmytro



2014-07-02 12:43 GMT+03:00 Altenkirch Thorsten <
psztxa at exmail.nottingham.ac.uk>:

> Thank you for the correction, Ulf.
>
> From: Ulf Norell <ulf.norell at gmail.com>
> Date: Wed, 2 Jul 2014 10:12:36 +0100
> To: txa <psztxa at exmail.nottingham.ac.uk>
> Cc: Sergei Meshveliani <mechvel at botik.ru>, "agda at lists.chalmers.se" <
> agda at lists.chalmers.se>
>
> Subject: Re: [Agda] termination by contradiction
>
>
>
>
> On Tue, Jul 1, 2014 at 10:04 PM, Altenkirch Thorsten <
> psztxa at exmail.nottingham.ac.uk> wrote:
>
>>
>>
>> On 01/07/2014 20:40, "Sergei Meshveliani" <mechvel at botik.ru> wrote:
>>
>> >
>> >Consider the example:
>> >
>> >  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) }
>> >
>>
>> In Agda we need to execute programs with variables. This is usually called
>> symbolic evaluation. It is important that symbolic evaluation terminates
>> otherwise the type checker will hang.
>>
>> In Agda every recursive program can be computed until it gets stuck.
>> However, it is not clear what this means for findFrom. If we recursively
>> unfold findFrom evaluation will not terminate.
>>
>> I guess you have an operational semantics in mind which does not unfold
>> under the case. While this seems reasonable (and solves the problem) it is
>> not without problems.
>>
>
> The problem isn't evaluation under the case. The case is just shorthand
> for a helper function that does the pattern matching, so you get the
> appropriate semantics. The problem is that findNatByContra never looks at
> the proof, so there is no guarantee that it's a closed proof (which
> Thorsten mentioned above). For instance,
>
> False : ℕ → Set
> False _ = ⊥
>
> decFalse : Decidable False
> decFalse _ = no (λ x → x)
>
> loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False
> loopy H = findNatByContra False decFalse H
>
> Here, loopy will happily evaluate forever with the hypothetical
> (classical) proof that there is a number satisfying False. There is no need
> to evaluate under the case since decFalse comes back 'no' for any number.
>
> / 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/20140702/65573f0d/attachment.html