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

All times shown according to UTC.

Time Nick Message
10:23 mornfall joined #darcs-theory
10:23 ertai joined #darcs-theory
10:23 lispy joined #darcs-theory
10:23 Igloo joined #darcs-theory
10:23 eelco joined #darcs-theory
10:23 Peng_ joined #darcs-theory
10:23 Heffalump joined #darcs-theory
10:37 kowey joined #darcs-theory
12:19 kowey joined #darcs-theory
16:54 arjanb joined #darcs-theory
22:49 Igloo Ho humm
22:51 arjanb ?
22:51 * Igloo is trying to think about how to handle http://urchin.earth.li/~ian/problem.png with permutivity proofs etc
22:52 Igloo The problem is that names don't really uniquely identify patches in sequences. The answer may be to give special names to patches that are in conflictors, but I'm not convinced
22:56 arjanb maybe have two kinds of sequences?
22:57 Igloo You mean only prove permutivity for sequences without repetition?
22:58 arjanb yeah
22:58 Igloo Then I can't use permutivity of patches to help prove permutivity of catches
22:59 Igloo I think the right thing to do is to just handle the same patch appearing multiple times in a sequence. It's just a pain because they can only appear twice, but that's much harder than once
23:04 arjanb i see patch sequences with inverses and the same patches again as a special construct:
23:04 arjanb p-a-b-*
23:04 arjanb *a-b*
23:04 arjanb \
23:04 arjanb a-b
23:05 arjanb a / fell off, so like a Z
23:06 Igloo You can commute patches, so it's not always that simple
23:09 arjanb hmm
23:10 arjanb i wonder if things will get easier if no conflictor has effect
23:11 Igloo how do you mean?
23:12 arjanb A + B =>  [;A][;B] <-> [;B][;A]
23:13 Igloo Oh, I see
23:14 Igloo It makes pull, unpull etc non-local, which would be a shame
23:14 Igloo Also, I don't think that this is causing a correctness problem, just a proof problem
23:17 arjanb pull will be as local as it was though not append only
23:17 Igloo Right, its changes won't be local
23:20 arjanb the problem i see in conflictors with effect is how to proof you never need to force commute in way they get a positive effect
23:21 Igloo I don't follow
23:24 arjanb the problem i got stuck on in the past with the commute that never fails for any permutation of a sequence
23:25 Igloo I don't think that you need all commutes in order to do all merges
23:28 arjanb quite possible, though trick to prove i guess