Camelia, the Perl 6 bug

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

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
07:50 arjanb joined #darcs-theory
09:15 DanielC joined #darcs-theory
09:29 tux_rocker joined #darcs-theory
13:13 kowey joined #darcs-theory
13:32 galbolle joined #darcs-theory
13:44 galbolle hi all
13:44 * DanielC waves
13:45 tux_rocker_outsi hi
14:02 galbolle Igloo: can you add a link to dic  darcs get http://patch-tag.com/publicrepos/dic  in the topic
14:02 galbolle please
14:05 Igloo Would it be better to make this the topic:
14:06 Igloo Patch Theory Semantics || http://wiki.darcs.net/DarcsWiki/PatchTheory || Log http://irclog.perlgeek.de/darcs-theory/
14:06 Igloo and add any missing links on http://wiki.darcs.net/DarcsWiki/PatchTheory ?
14:08 galbolle that'd be better, you're right
14:08 Topic for #darcs-theoryis now Patch Theory Semantics || http://wiki.darcs.net/DarcsWiki/PatchTheory || Log http://irclog.perlgeek.de/darcs-theory/
14:09 galbolle by the way, i haven't looked at your code yet, but are you sure you want inversion and not dependent induction?
14:09 Igloo I'm not doing induction
14:09 Igloo There's no recursion
14:09 galbolle also, uses of inversion are generally better strictly contained in some lemma
14:09 galbolle ok, i'll look at it later
14:09 Igloo OK, great, thanks
14:10 Igloo And I'll reply to your mail shortly
14:10 galbolle thanks too
14:10 galbolle no hurry, though…
14:38 galbolle joined #darcs-theory
15:03 Igloo galbolle: "de pied ferme"?
15:03 galbolle i don't know how to translate that
15:04 Igloo Err, OK  :-)
15:04 tux_rocker Igloo: should there be an accent on the last e or not?
15:04 galbolle no
15:04 galbolle with impatience
15:04 galbolle and ready to reply further
15:04 Igloo Ah, I see
15:05 galbolle maybe kowey would translate that better, as a native english speaker
15:24 galbolle igloo: regarding NamedPatchCommutePreservesCommute2, i'd only state one direction
15:24 galbolle (ie have it be …… ->  ((q1 <~?~> r1) -> (q3 <~?~> r3)).
15:24 galbolle and recover the other direction afterwards
15:25 Igloo OK
15:25 galbolle but it's a matter of taste
15:25 Igloo I don't think that affects my current problems, though. It would just remove a split; intro
15:26 galbolle yes
15:26 galbolle then afterward, i think o
15:26 galbolle i think most of your inversions should be destructs in fact
15:27 Igloo Is the only difference whether equality hypotheses get added?
15:29 galbolle i'm not exactly sure
15:29 galbolle inversion tries to do smart things
15:29 galbolle (which things mattam can tell you more exactly than me)
15:29 galbolle destruct is quite dumb
15:30 galbolle but if you only want to get the unnamed commute out of the named one, i think destruct is the right tactic
15:31 Igloo The thing is, when you have   q1 <~?~> r1   and the    p1 (q1 :> r1 :> [])    commute, when you take them both apart you have to be able to show that they have the same unnamed patches insde
15:33 galbolle hmm
15:33 galbolle but that's not the job of inversion
15:33 galbolle it's the job of unnamed_commute_consistent
15:34 Igloo If you use destruct on the above two you would get
15:34 Igloo uq1 <~?~>u ur1
15:35 Igloo up1 <~?~>u (uq1' :> ur1 :> [])
15:35 Igloo (roughly)
15:35 Igloo But we need uq1 = uq1'
15:38 galbolle i'm sorry, i don't get that
15:39 Igloo Do you mean you don't understand me?
15:41 galbolle no
15:41 galbolle yes i mean that
15:41 galbolle damned negative questions
15:41 Igloo :-)
15:41 Igloo Give me a tick
15:41 DanielC left #darcs-theory
15:43 galbolle on your drawing there's a commutation of p1 and q1 missing
15:44 galbolle there's a p5 from the end of q3 to the end of q1
15:45 galbolle also, if you use split, you should use it later
15:45 galbolle after you have milked the H_p1_q1_r1_commute_q3_r3_p3
15:45 galbolle to get your picture
15:46 * Igloo gets "Error: Expects a disjunctive pattern with 2 branches." when trying to make a simpler example
15:47 galbolle try not naming the variables you want inversion/destruct to produce
15:47 galbolle (don't use as)
15:47 Igloo Oh, it's because I used [] after intros, I think
15:48 galbolle then don't…
15:49 Igloo :-)
15:50 galbolle it's a good idea to do it, but you have to do a first pass without
15:50 galbolle then add it
15:50 galbolle because you can't guess them right the first time
15:51 Igloo No, I mean I write "intros [o op opq ..." instead of "intros o op opq ..."
15:51 Igloo s/write/wrote/
15:51 galbolle that is a bad idea
15:53 Igloo OK, maybe I'm wrong; maybe destruct is going to do the right thing after all
15:53 galbolle i think it is
15:53 Igloo http://hpaste.org/fastcgi/hpaste.fcgi/view?id=3838 is my failed attempt at a counter example, if you're interested
15:54 Igloo but when it gets to "destruct H as [r'].", H already has the p patch expanded
15:54 galbolle though you might want to start by inverting H_p1_q1_r1_commute_q3_r3_p3;
15:54 Igloo Why does inversion make sense in that case?
15:55 galbolle http://hpaste.org/fastcgi/hp​aste.fcgi/view?id=3839#a3839
15:55 galbolle because destruct does not work…
15:55 galbolle i was suprised to have to use it
15:55 Igloo Anyway, I know what I'll be start with at the hackathon now: Changing my proof to destruct and see whree that gets me
15:55 Igloo Thanks for your help!
15:56 galbolle i think you need inversion because destruct can't decide which branch of named_Patch_PatchSequence_Commute you're in
15:57 galbolle while inversion can get to the conclusion that it's not the null case
15:57 Igloo Ah, right
15:57 galbolle inversion is for doing destruct of a disjunctive case and weeding out stupid casse
15:57 galbolle cases
15:57 galbolle that's why you want it here
15:58 galbolle but namedCommute has only one case
15:58 galbolle so you want destruct
15:58 galbolle commutable sorry
16:01 galbolle with the start i pasted, it looks tedious but ok
18:07 rbuels joined #darcs-theory
18:07 rbuels left #darcs-theory
18:18 kowey joined #darcs-theory
22:40 kowey joined #darcs-theory

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary