[Agda] termination by contradiction

[Ulf Norell]

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