[Agda] termination by contradiction
gallais
guillaume.allais at strath.ac.uk
Thu Jul 3 15:24:06 CEST 2014
If you have large elimination, then you can simply use what Monin calls
a "small inversion" [1, 2]. If you don't, AFAIK you're in big trouble.
--
gallais
[1] http://hal.inria.fr/inria-00489412/en/
[2] http://lpaste.net/106851
On 03/07/14 13:46, Twan van Laarhoven wrote:
> There are lots of other empty types. For example `zero ≡ suc n` for a
> natural number n. Usually functions will not take an argument of this
> type, but they can have arguments that get this type after pattern
> matching. Here is a silly example.
>
> silly : ∀ {k} n → 2 * n ≡ suc k → n > 0
> silly zero ()
> silly (suc n) _ = s≤s z≤n
>
> I don't see how you can write this with ⊥-elim.
>
> Twan
>
> On 03/07/14 11:09, Sergei Meshveliani wrote:
>> 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
>>>
>>>
>>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list