[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