Time 
Nick 
Message 
01:16 

swc joined #darcstheory 
04:27 

mornfall joined #darcstheory 
04:27 

ertai joined #darcstheory 
04:28 

Igloo joined #darcstheory 
08:01 

arjanb joined #darcstheory 
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 #darcstheory 
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 counterexample 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 n1 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 workshopwards 
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 