[Agda] termination by contradiction

[Ulf Norell]

On Wed, Jul 2, 2014 at 5:36 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

>
> > 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).
>
> Please, what is a  closed proof?
>

A closed proof is a proof that does not contain any free variables.


> > 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.
>
> Can you, please, explain further?
>
> To apply  (loopy H),  one needs to provide
>                                    H : (∀ n → ¬ False n) → ⊥.
>
> And this is not possible, because its type normalizes to
>
> ((n : ℕ) → (False n → ⊥)) → ⊥,  and to  ((n : ℕ) → (⊥ → ⊥)) → ⊥,
>
> and the type  (n : ℕ) → (⊥ → ⊥)  has a value  (\n → id)  in it.
>
>
> As one cannot provide any argument value to `loopy',  how can it
> evaluate forever?
>

The problem is that in Agda programs need to terminate not only at run-time
when you apply them to actual arguments, but also at type checking-time when
the type checker runs programs to check for equality. For instance, suppose
you define loopy as above and then try to prove that loopy always returns 42

thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42
thm _ = refl

In this case the type checker needs to evaluate loopy in the context of the
free variable H to check if it normalises to 42. This evaluation will not
terminate
with your definition of findNatByContra.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140702/168bd7fe/attachment.html