[Agda] termination by contradiction

[Dmytro Starosud]

> But  thm  is useless, because the type for its first argument is empty.
⊥-elim
<http://www.cse.chalmers.se/~nad/listings/lib-0.7/Data.Empty.html#326> is
looking at you questionably?



2014-07-02 20:42 GMT+03:00 Sergei Meshveliani <mechvel at botik.ru>:

> On Wed, 2014-07-02 at 18:00 +0200, Ulf Norell wrote:
> >
> > [..]
>
>
> >         > 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.
> >
>
> But  thm  is useless, because the type for its first argument is empty.
> I hope, I can provide examples of practically usable programs which
> apply  findNatByContra.
>
> 1) But can `loopy' be introduced other than by a mistake?
>    Is there an example of a practically usable program which also uses
>    `loopy' ?
>
> 2) Suppose one introduces `loopy' by a mistake, and sets its various
> invocations, also by a mistake. What can happen then, in the worst case?
> Probably, the type checker will loop forever, and the user will
> interrupt the process of checking (as I did 10 minutes ago!).
> This will not make the whole usage worse, because there are many other
> ways in Agda to make the checker loop forever.
>
> Am I missing something?
>
> Regards,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> 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/b6f93f97/attachment-0001.html