[Agda] termination by contradiction

[Altenkirch Thorsten]

Thank you for the correction, Ulf.

From: Ulf Norell <ulf.norell at gmail.com<mailto:ulf.norell at gmail.com>>
Date: Wed, 2 Jul 2014 10:12:36 +0100
To: txa <psztxa at exmail.nottingham.ac.uk<mailto:psztxa at exmail.nottingham.ac.uk>>
Cc: Sergei Meshveliani <mechvel at botik.ru<mailto:mechvel at botik.ru>>, "agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>" <agda at lists.chalmers.se<mailto: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<mailto:psztxa at exmail.nottingham.ac.uk>> wrote:


On 01/07/2014 20:40, "Sergei Meshveliani" <mechvel at botik.ru<mailto: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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140702/a4a6109f/attachment.html