Time 
Nick 
Message 
07:45 

kowey joined #darcstheory 
11:26 

kowey joined #darcstheory 
17:35 

arjanb joined #darcstheory 
19:17 
* Heffalump 
looks at Igloo's png and is reminded of the game in the '06 ICFP contest 
19:17 
Igloo 
heh 
19:19 
Heffalump 
can you repeat your statement above with the w,x,y,z from the picture? 
19:21 
Igloo 
The problem is: Prove that y and z commute in the first line iff they commute in the last line 
19:22 
Igloo 
I think that you need to know <xy,z> <> <z',_> <=> <y'x',z> <> <z',_> 
19:22 
Heffalump 
(FWIW, my theory attempt assumes that property as an axiom) 
19:22 
Igloo 
(where the two z's are the same) 
19:22 
Heffalump 
the general property that two patches commute consistently. 
19:23 
Heffalump 
so is there some simpler version of that picture (say with only one other patch) that you can prove it for? 
19:24 
Igloo 
With 1 other patch it's the 3patchpermutivity axiom 
19:26 
Heffalump 
well, anyway, I think you should insist on patches being unique for a given name+context :) 
19:27 
Igloo 
I'm going to want to prove it for catches too, so I need to be able to prove it anyway 
19:28 
Heffalump 
to prove what? 
19:28 
Igloo 
To prove that catches are unique for a given name+context 
19:29 
Heffalump 
oh, right 
19:29 
Heffalump 
if you require it for catches you clearly require it for patches 
19:30 
Heffalump 
so the only question is whether it's an axiom or whether there's some lowerlevel axiom 
19:30 
Igloo 
Well, I only require it if the permutivity proof requires it. But I think that it does. 
19:30 
Igloo 
I think it follows from the 3patch case, like permutivity does 
19:31 
Heffalump 
I think the two of us have slightly different views of permutivity. 
19:31 
Igloo 
Oh? 
19:31 
Heffalump 
I say that it means you get the same patches back, whereas you say it just means that the commutes are consistent. 
19:31 
Heffalump 
i.e. their failure or otherwise 
19:31 
Igloo 
Didn't you say that you had an axiom that you get the same patches back? 
19:32 
Igloo 
Oh, or did you just mean the 3patch case above? 
19:32 
Heffalump 
sorry, I confused myself. 
19:32 
Heffalump 
I have an axiom that commutes happen consistently. 
19:32 
Heffalump 
i.e. fail or not 
19:33 
Heffalump 
I also have 3way permutivity (i.e. that you get the same patches back) as an axiom 
19:33 
Heffalump 
From that I prove nway. 
19:33 
Igloo 
OK. So I definitely need that commutes happen consistently for catches, because otherwise you can't do merges, so I definitely need to be able to prove that 
19:34 
Igloo 
I thought that your permutivity proof was for both, not for one assuming the other 
19:34 
Heffalump 
I imagine it's possible to reduce the axiom about consistency to something less global. 
19:35 
Heffalump 
Which is what you seem to be suggesting how to do. 
19:35 
Igloo 
Right 