[Agda] termination by contradiction

[Sergei Meshveliani]

On Wed, 2014-07-02 at 22:38 +0300, Dmytro Starosud wrote:
> > But  thm  is useless, because the type for its first argument is
> empty.
> 
> ⊥-elim is looking at you questionably?
> 

⊥-elim  somehow fills a certain small gap in Agda.
But I wonder, having  ⊥-elim,  do we need other functions using any
argument type which is provably empty?  



> 
> 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
>         
> 
>