# IRC log for #darcs-theory, 2008-09-21

All times shown according to UTC.

Time Nick Message
01:16 swc joined #darcs-theory
04:27 mornfall joined #darcs-theory
04:27 ertai joined #darcs-theory
04:28 Igloo joined #darcs-theory
08:01 arjanb joined #darcs-theory
13:20 Heffalump Igloo: can you summarise again what properties you think are sufficient to prove that if two patches commute, they commute in all contexts?
13:23 kowey joined #darcs-theory
13:41 Igloo Heffalump: http://urchin.earth.li/~ian/sufficient.png
13:42 Igloo Where x <-?-> y holds iff xy <-> y'x'
13:43 Igloo Heffalump: Plus things like (xy <-> y'x') <=> (y'x' <-> xy), of course
14:03 arjanb the whole point of second is to say p' is the same in both commutes right?
14:03 Igloo Yup
14:07 Igloo I'm not sure what the proof looks like. Perhaps induction on the number of patches on the initial sequence
14:08 Igloo Showing that you can add a patch to the end of the sequence at the start. and then show that you can undo all the commutes that it does one at a time, or something
14:10 Igloo Hmm, maybe not. I'll need to think about it more
14:10 Heffalump thanks
14:13 arjanb i wonder if there's anything to prove by contradiction, i have trouble imagining the case where the order of commutes makes a difference
14:16 Igloo Contradiction would be that there was a counter-example with either fewest commutes, or fewest involved patches, I think
14:16 Igloo And fewest commutes sounds hard to disprove
14:18 Igloo fewest involved patches sounds like it might be an easy way to think about what I was thinkg about with induction above
14:18 Igloo s/easy/easier/
14:20 Igloo I'm stil not sure that it's easy, though
14:27 Heffalump can you state the result in your notation, too?
14:35 Igloo Third line of http://urchin.earth.li/~ian/sufficient2.png
14:37 Igloo (we'll actually have to worry about pulls and unpulls too at some point, but the above is the main part)
14:39 Heffalump is <p,qr> <-> <q'r',p'> shorthand for two actual commutes
14:39 Igloo It's patch sequence commute
14:39 Igloo So yes
14:40 Igloo <p,q> <-> <q',p''> and <p'',r> <-> <r',p'>
14:41 Heffalump ok, so the problem with connecting 1 to 3 is that some random shit might happen in the middle while q and r are separated
14:41 Igloo Yup
14:41 Heffalump thakns
14:41 Igloo Well, if it only happens in the middle then I think it's easy
14:42 Heffalump but the things might get commuted with p and q too
14:42 Heffalump so yeah, not just in the middle
14:42 Igloo Oh, no, it's only trivial if all the patches are going one way
14:42 Igloo Right
14:42 Heffalump I think this is why I decided to just treat (3) as an axiom.
14:42 Igloo Right, but I need it for catches, and I can't have axioms for catches
14:43 Heffalump the issue is whether to have (3) as an axiom or (1)+(2),assuming for the moment that (1)+(2) == (3)
14:43 Heffalump for catches, you need to prove the "axioms" based on the properties of patches
14:44 Heffalump (this is why I called axioms "assumed properties" in my document)
14:44 Igloo Right, but the way I plan to show (3) for catches is to show (1) and (2) and then use the proof for (3)
14:45 Heffalump sure, but the issue is whether (1)+(2) are easier to show for catches or (3) is, it's not that (3) is impossible
14:46 Igloo Right. It would also be easier on the patch supplier if they didn't have to check that (3) holds
14:46 Heffalump yeah
14:46 * Heffalump is all in favour of (1)+(2) if it's right.
14:47 arjanb maybe you also need an axiom that a commute is local
14:47 Igloo What do you mean?
14:48 arjanb that a commute within a patch sequence doesn't affect the rest of the sequence
14:48 Igloo commute is defined as local
14:49 arjanb ok
14:50 Igloo <->* allows a series of patch pair commutes inside a sequence
14:50 Heffalump I think distinguishing <-> and lifted <->^ like I do is quite helpful
14:50 Igloo What is <->^?
14:51 Heffalump it allows a commute somewhere in a sequence of patches
14:51 Igloo Ah, right
14:52 Heffalump it means you can use induction on its derivation rather than waving your hands
14:53 Igloo I don't think that induction on that is useful here, because the n-1 case doesn't have q and r adjacent
14:53 Heffalump is the idea of generalising too much for you? :-)
14:53 Heffalump (I don't know how to generailse yet)
14:54 Heffalump but dismissing the entire proof technique is probably a bit much
14:54 Igloo Please do prove me wrong  :-)
14:56 * Heffalump wanders ML workshop-wards
14:56 Igloo Enjoy!
16:26 Igloo OK, I think I know how to do it: You show that you can always commute the rightmost patch out to the right after each internal commute
17:10 Igloo And I think that you can show that pull/unpull are OK by showing that it can always commute into its minimal context, and that it is always the same in the minimal context
17:10 Igloo Which means we still need to show that name+context uniquely determines the patch
17:11 Igloo But a similar argument of commuting something right ought to work for that
17:34 arjanb if you take as name the patch with it's minimal context at recording then rest could be inductivily adding more context
17:48 arjanb the only way to add context is to commute other patches in which can commute out in any order so you can always get back to the same minimal context
17:49 Igloo We don't want that to be an axiom, though
17:52 arjanb the naming?
17:52 Igloo That a unique minimal context exists
17:54 arjanb that's not needed i think
17:55 Igloo Oh, I misunderstood what you said, sorry
17:56 arjanb you only have to prove you can always get back to the minimal context at record time