# IRC log for #darcs-theory, 2009-04-24

All times shown according to UTC.

Time Nick Message
07:39 ordwidr joined #darcs-theory
07:55 kowey joined #darcs-theory
09:04 tux_rocker joined #darcs-theory
11:49 ordnungswidrig left #darcs-theory
12:42 kowey joined #darcs-theory
14:40 kowey joined #darcs-theory
15:20 Igloo If anyone wants a little challenge, a proof that you can't commute ABCD (where all the patches depend on all earlier patches) into BDAC by doing only merges and non-conflict-introducing commutes would be very nice
16:26 kowey joined #darcs-theory
16:33 arjanb joined #darcs-theory
18:31 Heffalump a formal proof?
18:32 Heffalump it seems intuitively obvious seeing as no commutes are valid at all..
18:34 Heffalump just consider any commute sequence, and consider the fact that you'd have to swap A and B at some point.
19:21 Igloo I'll think more about my question and reformulate it later
19:24 Igloo In the mean time, I have another question:
19:25 Igloo Is it correct to say that the camp proof are proof-theoretical, and what Andres and Wouter were doing is model-theoretic?
20:06 Heffalump I don't really understand those terms well enough to know. But possibly.
20:06 Heffalump What I'm trying to do is most like what Andres and Wouter were doing, I think.
20:15 Igloo OK, ta
20:43 Igloo Heffalump: OK, suppose we have AB where B depends on A
20:44 Igloo Now, record A^ in one repo and B in another
20:44 Igloo Then merging these repos means creating catches B' and A' such that AB <-> B'A', right?
20:45 Igloo So I want to know that you can't do something like that to get from ABCD to B'D'A'C'
20:49 Heffalump named or unnamed patches?
20:50 Igloo Why does it matter?
20:50 Heffalump doesn't that affect what A^ is?
20:50 Heffalump perhaps not
20:51 Igloo Assume unnamed. I don't think it matters.
21:03 arjanb isn't it enough to show no operation reorders dependent patches?
21:16 Igloo But that's not true when you can do merges
21:16 Igloo Actually, I'm pretty sure the above is false
21:17 Igloo In the same way I get A and B to commute, you can get C and D to commute, and then you merge (AB)^ and CD, and everything commutes
21:17 * Igloo is going to have to work out what the conflictors look like
21:17 Heffalump errm, so then conflictors support arbitrary commutes?
21:17 Igloo Well, that's what I'm trying to work out
21:18 arjanb patches in a merge never depend on each other
21:18 Heffalump the merge is A^ + B
21:18 Heffalump not A + B
21:18 Heffalump etc
21:19 Heffalump so if conflictors support arbitrary commutes, they also have to behave properly when uncommuted...
21:19 Heffalump or, perhaps they don't support that
21:19 Igloo Oh no, wait, you actually get AB' and BA', don't you
21:20 Heffalump when?
21:20 * Igloo has confused himself
21:23 Igloo OK, ignore my "Oh no, wait" line