# IRC log for #darcs-theory, 2009-01-12

All times shown according to UTC.

Time Nick Message
15:40 thorkilnaur joined #darcs-theory
19:22 arjanb joined #darcs-theory
21:00 * Heffalump thinks he has identified 26 distinct ways of commuting two move patches
21:01 arjanb how do you know you haven't missed any?
21:01 Heffalump I don't
21:02 Heffalump Once I've finished with the details of them I'll think about how to gain confidence that I haven't..
21:02 Heffalump But also some cases may be subjective
21:04 arjanb i hope some of them can be collapsed in a more general ones, because 26 is too much for intuition
21:05 Heffalump well, do you agree there are two cases for hunk-hunk commute?
21:05 arjanb yes
21:05 Heffalump ok, so for move-move commute I've so far identified (2^2+1)^2+1 cases
21:06 Heffalump the 2 is exactly the same as for hunk-hunk commute, i.e. before and after cases
21:06 Heffalump but then you have to consider both the source and the destination of each move, so it gets squared twice
21:06 Heffalump and there's also an "inside" case where one move is nested inside the other
21:06 Heffalump and that pops up in a few places
21:08 arjanb i see
21:08 Heffalump I'm working it out programmatically, so hopefully someone else can look at it all themselves without too much pain.
21:08 arjanb so using a theorem prover will be a must to get it right..
21:09 Heffalump I think so, yes.
21:09 Heffalump but I'm not sure how you formulate a completeness property with a theorem prover
21:09 * Igloo wants something like Hoare triples for Haskell