[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy
theory & advantage of UF/Coq
Conor McBride
conor at strictlypositive.org
Wed Jan 8 10:50:23 CET 2014
On 7 Jan 2014, at 22:47, Altenkirch Thorsten <psztxa at exmail.nottingham.ac.uk> wrote:
> Hi Conor,
>
> I am sure this must be a stupid question but why is this not covered
> by your result that pattern matching can be reduced to eliminators + K?
The recursive call isn't covered by the inductive hypothesis. The direct version
gives no account of the inductive hypothesis *at all*, hence the whole mess.
>>>> moo (wrap f) = noo (Zero -> WOne) myIso f
>>>> noo .WOne Refl x = moo x
The recursive call
moo x
is really a recursive call
moo (subst myIso ... f)
but the inductive hypothesis tells us just that we can call moo on outputs of f.
Bottom line: it's not structurally recursive.
Cheers
Conor
>>
>> moo's input is bigger than the third argument in its noo call
>> noo's third input is the same as the argument in its moo call
>>
>> Size-change termination, how are ye?
>>
>> When you do the translation to eliminators, you're obliged to
>> show how recursive calls correspond to invocations of the
>> inductive hypothesis: here that's just not going to happen.
>> Transporting f across myIso does indeed give an element of
>> WOne (your Box), but that does not make a nullary inductive
>> hypothesis any easier to invoke.
>>
>> I'd quite like to see us defining a type theory in which the
>> only checking is type checking, then using it as a target for
>> elaboration. Eliminators are one candidate, but there are
>> others. Sized types are certainly another strong candidate.
>> I'm also interested to see whether there are "locally clocked"
>> explanations for termination, as there seem to be for
>> productivity.
>>
>> Interesting times
>>
>> Conor
>>
>>
>>>>
>>>> bad : Zero
>>>> bad = moo (wrap \ ())
>>>>
>>>>
>>>>
>>>>> T.
>>>>>
>>>>>> I am also not sure how specific the problem is to univalence. As Cody
>>>>>> said, I would expect to find some set-theoretical models where the
>>>>>> equality holds. So being able to prove the negation is disturbing.
>>>>>>
>>>>>> Maxime.
>>>>>>
>>>>>> On 01/06/2014 07:23 PM, Abhishek Anand wrote:
>>>>>>> It is known that UIP is inconsistent with univalence.
>>>>>>> Does this typecheck even after disabling UIP(==K axiom?) ?
>>>>>>> I might be wrong, but I think that UIP is baked into the typechecker
>>>>>>> of Agda.
>>>>>>> But, UIP can be disabled somehow?
>>>>>>>
>>>>>>>
>>>>>>> -- Abhishek
>>>>>>> http://www.cs.cornell.edu/~aa755/
>>>>>>> <http://www.cs.cornell.edu/%7Eaa755/>
>>>>>>>
>>>>>>>
>>>>>>> On Mon, Jan 6, 2014 at 3:42 PM, Maxime Dénès <mail at maximedenes.fr
>>>>>>> <mailto:mail at maximedenes.fr>> wrote:
>>>>>>>
>>>>>>> Bingo, Agda seems to have the same problem:
>>>>>>>
>>>>>>> module Termination where
>>>>>>>
>>>>>>> open import Relation.Binary.Core
>>>>>>>
>>>>>>> data Empty : Set where
>>>>>>>
>>>>>>> data Box : Set where
>>>>>>> wrap : (Empty → Box) → Box
>>>>>>>
>>>>>>> postulate
>>>>>>> iso : (Empty → Box) ≡ Box
>>>>>>>
>>>>>>> loop : Box -> Empty
>>>>>>> loop (wrap x) rewrite iso = loop x
>>>>>>>
>>>>>>> gift : Empty → Box
>>>>>>> gift ()
>>>>>>>
>>>>>>> bug : Empty
>>>>>>> bug = loop (wrap gift)
>>>>>>>
>>>>>>> However, I may be missing something due to my ignorance of Agda.
>>>>>>> It may be well known that the axiom I introduced is inconsistent.
>>>>>>> Forgive me if it is the case.
>>>>>>>
>>>>>>> Maxime.
>>>>>>>
>>>>>>>
>>>>>>> On 01/06/2014 01:15 PM, Maxime Dénès wrote:
>>>>>>>
>>>>>>> The anti-extensionality bug is indeed related to termination.
>>>>>>> More precisely, it is the subterm relation used by the guard
>>>>>>> checker which is not defined quite the right way on dependent
>>>>>>> pattern matching.
>>>>>>>
>>>>>>> It is not too hard to fix (we have a patch), but doing so
>>>>>>> without ruling out any interesting legitimate example (dealing
>>>>>>> with recursion on dependently typed data structures) is more
>>>>>>> challenging.
>>>>>>>
>>>>>>> I am also curious as to whether Agda is impacted. Let's try it
>>>>>>> :)
>>>>>>>
>>>>>>> Maxime.
>>>>>>>
>>>>>>> On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:
>>>>>>>
>>>>>>> Which bug was this?
>>>>>>>
>>>>>>> I only saw the one which allowed you to prove
>>>>>>> anti-extensionality? But
>>>>>>> this wasn't related to termination, or?
>>>>>>>
>>>>>>> Thorsten
>>>>>>>
>>>>>>> On 06/01/2014 16:54, "Cody Roux" <cody.roux at andrew.cmu.edu
>>>>>>> <mailto:cody.roux at andrew.cmu.edu>> wrote:
>>>>>>>
>>>>>>> Nice summary!
>>>>>>>
>>>>>>>
>>>>>>> On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
>>>>>>>
>>>>>>> Agda enforces termination via a termination
>>>>>>> checker which is more
>>>>>>> flexible but I think less principled than Coq's
>>>>>>> approach.
>>>>>>>
>>>>>>> That's a bit scary given that there was an
>>>>>>> inconsistency found in
>>>>>>> the Coq termination checker just a couple of weeks ago
>>>>>>> :)
>>>>>>>
>>>>>>> BTW, has anyone tried reproducing the bug in Agda?
>>>>>>>
>>>>>>>
>>>>>>> Cody
>>>>>>>
>>>>>>> This message and any attachment are intended solely for
>>>>>>> the addressee and may contain confidential information. If
>>>>>>> you have received this message in error, please send it
>>>>>>> back to me, and immediately delete it. Please do not use,
>>>>>>> copy or disclose the information contained in this message
>>>>>>> or in any attachment. Any views or opinions expressed by
>>>>>>> the author of this email do not necessarily reflect the
>>>>>>> views of the University of Nottingham.
>>>>>>>
>>>>>>> This message has been checked for viruses but the contents
>>>>>>> of an attachment
>>>>>>> may still contain software viruses which could damage your
>>>>>>> computer system, you are advised to perform your own
>>>>>>> checks. Email communications with the University of
>>>>>>> Nottingham may be monitored as permitted by UK
>>>>>>> legislation.
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>> _______________________________________________
>>>>>>> Agda mailing list
>>>>>>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>>>
>>>>>>>
>>>>>>> _______________________________________________
>>>>>>> Agda mailing list
>>>>>>> Agda at lists.chalmers.se <mailto: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