[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy
theory & advantage of UF/Coq
Jesper Cockx
Jesper at sikanda.be
Wed Jan 8 11:35:04 CET 2014
I'm trying to get a better understanding of the problem by manually
translating the definition down to eliminators. First, here's a version of
Conor's example without mutual induction:
noo : (X : Set) -> (WOne <-> X) -> X -> Zero
noo .WOne Refl (wrap f) = noo (Zero → WOne) myIso f
And here are the standard eliminators for WOne and <->:
WOne-elim : (P : WOne -> Set) ->
(m : (f : Zero -> WOne)
(h : (z : Zero) -> P (f z)) ->
P (wrap f)) ->
(x : WOne) -> P x
WOne-elim P m (wrap f) = m f (λ z → WOne-elim P m (f z))
<->-elim : (X : Set) (P : (Y : Set) -> X <-> Y -> Set) ->
(m : P X Refl) ->
(Y : Set) (E : X <-> Y) -> P Y E
<->-elim X P m .X Refl = m
Now I try to write noo using only these eliminators, to see what goes wrong:
noo' : (X : Set) -> (WOne <-> X) -> X -> Zero
noo' X E x = <->-elim WOne (λ Y _ → Y → Zero) subgoal X E x
where
subgoal : WOne -> Zero
subgoal = (WOne-elim (λ _ → Zero) (λ f h → h {!!}))
What I understand of it, is that the order in which we apply the
eliminators is important here. We start with x : X, so we cannot apply
WOne-elim directly. So we first apply <->-elim instead, leaving the subgoal
? : WOne -> Zero. Now we can apply WOne-elim, however we are only allowed
to make recursive calls to the subgoal, not to noo' itself. In particular,
we cannot supply myIso as the argument for WOne <-> X, as it is already
fixed to be Refl. I wonder if this problem was already present in
'Eliminating Dependent Pattern Matching', or was introduced later by the
termination checker of Agda? This is certainly all very interesting...
Jesper
On Wed, Jan 8, 2014 at 11:05 AM, Altenkirch Thorsten <
psztxa at exmail.nottingham.ac.uk> wrote:
> P.S. An attempt at a summary:
>
> We already knew that pattern matching is incompatible with univalence
> because we can prove K.
>
> Now, due to the example by Maxime (and Conor) there is another
> incompatibilty which arises from pattern matching making things appear
> structurally recursive which shouldn't be.
>
> This one is not covered by K and it is another example where pattern
> matching is non-conservative over the standard eliminators (I guess we
> could invent a version of combinators which allow us to use propositional
> equality of types during recursion).
>
> As a consequence it also affects Coq, which always ruled out K but not
> this one.
>
> This is clearly a bug (has anybody filed a bug report) which should be
> fixed as a matter of urgency. Any proposals?
>
> Thorsten
>
>
> On 08/01/2014 09:52, "Altenkirch Thorsten"
> <psztxa at exmail.nottingham.ac.uk> wrote:
>
> >On 07/01/2014 23:03, "Conor McBride" <conor at strictlypositive.org> wrote:
> >
> >>
> >>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.
> >
> >I know this - this was precisely the comment I made in my reply to Maxime.
> >
> >However, it seems I am a victim of my own propaganda: I was always
> >thinking that Conor's result tells us that we can replace pattern matching
> >(with guarded recursion) by elimination constants.
> >
> >However, this example shows that this is not true. Once we perform the
> >unification required by pattern matching we obtain a a term which "looks"
> >as if it is structurally smaller even though it isn't.
> >
> >One obvious question is how we can recognize good instances of pattern
> >matching from bad ones.
> >
> >This also increases the argument in favour of a safe version of pattern
> >matching which is evidence producing. One of my new students, Gabe
> >Dijkstra, is working on this - mainly triggered by the without-K issue.
> >However, as we see now there are other issues which went unnoticed.
> >
> >Cheers,
> >Thorsten
> >
> >>
> >>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
> >>>>>
> >>>>
> >>>
> >>
> >
> >
>
>
> _______________________________________________
> 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/20140108/b6d1e241/attachment-0001.html
More information about the Agda
mailing list