[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy
theory & advantage of UF/Coq
Conor McBride
conor at strictlypositive.org
Wed Jan 8 21:41:37 CET 2014
On 8 Jan 2014, at 14:20, Jesper Cockx <Jesper at sikanda.be> wrote:
> Conor: I think it is not fair to say that noo is not structurally recursive; it should be totally fine according to definition 6 in "Eliminating Dependent Pattern Matching".
One reason why my brief career as a singer-songwriter was curtailed is that
I could never remember the words, but I think it highly unlikely that the
paper we wrote back then made any kind of assurance about mutual definitions
like moo and noo. If I did, then perhaps I join the good company in error,
for which I apologize.
I quite agree that the definition of "structurally smaller" we gave does say
that
f < wrap f
where f amounts to a collections of (no) things, all of which are smaller
than (wrap f). NOWHERE is it said that transporting f with respect to an
equation on types respects structural ordering relations, and ESPECIALLY
IN THE PRESENCE OF UNIVALENCE that is OBVIOUS NONSENSE.
Isomorphisms of types do not necessarily preserve the subterm structure
of types that we rely on to validate computation. Correspondingly, we
should expect some turbulence. Consider, for example, the fact that
natural numbers are isomorphic to binary trees whose nodes are labelled
with binary numbers. Does such an isomorphism entitle us, when writing
a function on trees to "structural recursion" on the tree-meaning of a
node label? Wlog, we have some
iso : Tree Nat <-> Nat
such that
transport (sym iso) 666 = node leaf 666 leaf
It's clearly inappropriate to consider the "tree" 666 (via iso) a
structural subterm of (node leaf 666 leaf).
> Looking at the proof of theorem 24 in the same paper, I see one implicit assumption that is not mentioned in the statement of the theorem itself and also currently not checked by Agda. The extra condition is that the type of the argument on which the function is structurally recursive should be a data type D vs. The definition of noo fails this condition, since
since noo is not moo
> it is structurally recursive on its third argument, whose type X is not a data type (at least not before pattern matching).
It's more complex than that, once we are allowed to shunt stuff around
by isomorphisms which are not obliged to respect structural orderings.
Eliminators are ok because they fix the "view" of the datatype for the
whole of the recursion. They don't allow you to make up spurious,
allegedly smaller, elements of the type by shipping stuff across
isomorphisms.
Careful now
Conor
>
>
> Jesper
>
>
> On Wed, Jan 8, 2014 at 11:35 AM, Jesper Cockx <Jesper at sikanda.be> wrote:
> 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
>
>
>
More information about the Agda
mailing list