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

All times shown according to UTC.

Time Nick Message
07:45 kowey joined #darcs-theory
11:26 kowey joined #darcs-theory
17:35 arjanb joined #darcs-theory
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 3-patch-permutivity 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 lower-level 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 3-patch 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 3-patch 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 3-way permutivity (i.e. that you get the same patches back) as an axiom
19:33 Heffalump From that I prove n-way.
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