# IRC log for #darcs-theory, 2009-05-08

All times shown according to UTC.

Time Nick Message
07:47 ordnungswidrig joined #darcs-theory
07:47 ordnungswidrig left #darcs-theory
10:56 gal_bolle joined #darcs-theory
11:24 tux_rocker joined #darcs-theory
11:25 gal_bolle stupid question of vocabulary: how would you say "to pull on a string to make it straight" ?
12:07 Igloo straighten?
12:07 Igloo I'm not really sure what you mean
12:07 Igloo tauten?
12:07 gal_bolle i was hoping to get a synonym for straighten
12:08 gal_bolle tauten seems nice
12:08 gal_bolle btw, i'm almost done
12:08 gal_bolle for an ever-decreasing value of almost
12:08 Igloo :-)
12:09 Igloo Are you sure about that? I'm sure my "amount left to do" wasn't monotonically decreasing  :-)
12:09 gal_bolle i think it's going to be from now on
12:55 gal_bolle did you do the generalization of your theorem?
13:10 Igloo No, I've done nothing since my e-mail
13:38 gal_bolle argl
13:38 gal_bolle unforeseen hard lemma
13:38 Igloo I hate to say I told you so...  :-)
13:41 gal_bolle it's either tedious or super-tedious
13:41 gal_bolle let us hope it is only tedious
13:41 Igloo What is it?
13:42 gal_bolle so my plan is to prove these shuffle_*_tauten lemmas
13:43 gal_bolle which say that if you can go from one sequence to another by a sequence of commutaitions, there is a way to do it without stupid commutations
13:43 gal_bolle like pq -> q'p' -> pq
13:43 gal_bolle or worse
13:44 Igloo *nod*
13:44 gal_bolle the * corresponds to whether you are marking 1 or 2 patches and following them through the commute
13:44 gal_bolle (it's either mark_one or mark_two)
13:45 gal_bolle now i want to say that if start : p : middle : q : tail goes to
13:45 gal_bolle start' : p' : middle' : q' : tail'
13:45 gal_bolle and i know how to tauten that sequence of commutes
13:46 gal_bolle then i know how to tauten the following:
13:46 gal_bolle tail^ : q^ : middle^ : p^ : start^ goes to tail'^ : q'^ : middle'^ : p'^ : start'^
13:47 gal_bolle it's painful because my tauten types (which was called rectify until now, if you peeked at my code) specify an arbitrary order for the commutes
13:47 gal_bolle ie, you're supposed to mix start with middle, then the result with tail
13:48 gal_bolle and of course, inverting everyone gives the wrong order
13:48 gal_bolle so i have to mass-apply commute-consistent
13:51 Igloo Ah, I see
16:49 arjanb joined #darcs-theory