Camelia, the Perl 6 bug

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

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

All times shown according to UTC.

Time Nick Message
08:17 kowey joined #darcs-theory
12:57 kowey joined #darcs-theory
16:55 arjanb joined #darcs-theory
19:38 kowey joined #darcs-theory
19:56 Heffalump Igloo: I've had a bit of a look at camp-theory now.
19:56 * Heffalump goes to find the notes he wrote
19:58 Igloo Cool
20:01 Heffalump the whole positive/negative name thing isn't very satisfactory.
20:01 Heffalump should axiom 4.3 say n(p) = -n(p^-1) ?
20:01 Heffalump (it currently says n(p) = n(p^-1)
20:02 Igloo Yes, it should
20:02 Igloo Why is it unsatisfactory?
20:03 Heffalump does negativeness have any special meaning when putting things in sets?
20:03 Heffalump Or is it banned to have p, p^-1, p, p^-1 etc in a repo?
20:04 Igloo You can't have catches named n n^ n in a repo
20:04 Heffalump so a primitive patch can't be named n^ ?
20:05 Igloo I'm lost now
20:05 Heffalump oh, never mind
20:05 Heffalump I was confusing catches with conflictors
20:05 Heffalump ok, so sets of names don't care about positive or negativeness.
20:06 Igloo Oh, except you can't have negative n in a context without also having positive n
20:06 Heffalump ok, so that's how I find them unsatisfactory, they're rather vague.
20:07 Igloo So what would you suggest instead?
20:08 Heffalump perhaps just be less vague. e.g. clarify the context restriction.
20:08 Igloo OK
20:09 Heffalump I'm trying to send you a few tiny patches, but mail on my laptop is misbehaving.
20:10 Igloo Cool, thanks
20:12 Heffalump a general comment: it would be nice if the theory was sort of modular or parametrisable.
20:12 Igloo *nod*, I'm currently rewriting it to be clearer on what the inputs and outputs are
20:13 Heffalump you might also want to add the n-way permutivity result somewhere (though my proof is still incomplete, but I'm convinced it's right, just a pain to express)
20:14 Igloo I think you can actually show that patches in a sequence make a poset given the patch commute associativity axiom
20:15 Heffalump a poset on what ordering, dependency?
20:15 Igloo Yup
20:15 Igloo Which is equivalent to n-way permutivity, I guess, but I think a more useful way of saying it
20:15 Heffalump that's a poset on the name, not the actual patch, presumably?
20:15 Heffalump really?
20:15 Igloo Yup
20:16 Igloo Yeah; it follows from that that you have minimal contexts, and that you can commute common patches to the left when doing merges
20:17 Heffalump I don't understand how it being a poset on the name helps you show any permutivity properties. (I prefer that name to associativity, because associativity is a(bc) = (ab)c and I can't see how that's is what's happening here)
20:18 Heffalump also, you don't seem to have any results that if something is true of patches it's true of all patches with the same name.
20:18 Igloo What sort of thing?
20:18 Heffalump commutes succeeding/failing, for example
20:18 Igloo permutivity basically says that if X Y commutes, then X'Y' commutes, right?
20:19 Heffalump no, it's the n-way version of your associativity rule.
20:19 Igloo That's what my associativity rules says
20:19 Igloo Oh, there's also that patches with the same name are identical if they are in the same context; is that what you mean?
20:20 Heffalump well, you can get that as a derived rule of it
20:20 Heffalump no, I mean that if pq commute, then p'q' commute if they have the same name.
20:20 Heffalump i.e. what you just said
20:20 Igloo OK, so that's what named patch sequences making a poset says
20:21 Heffalump what is the poset on?
20:21 Heffalump names, or patches?
20:21 Igloo Names
20:21 Igloo Well, the names of the named patches
20:22 Heffalump then what you are saying is that you can define the success or failure of commutation of names.
20:22 Heffalump And that this is a consistent thing.
20:22 Igloo So it says "Any patch called n depends on any patch called m"
20:22 Heffalump ok, and how do you show that result?
20:22 Heffalump that's not the same as "names form a poset", though.
20:23 Igloo It follows from 3 patch permutivity, I believe
20:23 Heffalump it's a necessary condition for a poset to even make sense.
20:23 Heffalump another issue is that 3 patch permutivity doesn't talk about failure.
20:23 Igloo Yes it does, there's an if-or-only-if in the middle
20:23 Heffalump hmm, perhaps it doesn't need to.
20:23 Heffalump don't you need to relate failure between the specific commutes, though?
20:24 Igloo Actually, the current axiom says too much. You only need 4 sides of the hexagon
20:24 Heffalump so you're suggesting removing two of the conjuncts on one side of the iff, and making it a only if instead?
20:24 Igloo You need:   In pqr, if q and r can commute, and p commutes past them, then q' and r' commute
20:25 Heffalump anyway, you do need the 6 sides, because you need to show that you get back to exactly the same patches.
20:25 Heffalump Not just that it succeeds.
20:25 Igloo Or perhaps better phrased: If <p,qr> <-> <q'r',p> then qr commutes iff q'r' commutes
20:26 Igloo I don't think you actually need to get back to exactly the same patches
20:26 Heffalump why not?
20:26 Igloo Well, what goes wrong if you don't?
20:27 Heffalump you need a result that two repos are the same if they have the same sequence of names
20:27 Heffalump that's one of the nice consistency properties of darcs
20:27 Heffalump i.e. it's useful for the outside world
20:28 Igloo But I don't show that pq and qp are "the same" either
20:28 Heffalump perhaps permutivity is a good candidate for modular bits of the theory :-)
20:29 Heffalump but actually regardless of whether different sequences of the same set have the same "effect" or not, I think it's important for the same sequences to be indistinguishable.
20:29 Heffalump Otherwise I can't see how you'll ever prove that there's only one possible answer that an algorithm can produce.
20:30 * Heffalump gives up on his laptop and moves the patches to his desktop to send, and does so
20:30 Igloo The associativity/permutivity/poset axiom shows that they are indistinguishable as far as commute is concerned
20:31 Heffalump ok, then you need to define an equivalence class.
20:31 Igloo An equivalence class of what?
20:31 Heffalump patches - two patches are equivalent if they have the same name and context.
20:32 Heffalump otherwise your "indistinguishable" comment isn't formalised
20:32 Igloo Huh? The axiom formalises it
20:33 Heffalump only locally
20:33 Heffalump you need to prove it applies globally
20:33 Igloo Right, so I need to prove that the 3-way axiom actually does make a poset
20:34 Heffalump ok, so can you sketch that proof?
20:34 Heffalump and be precise about when you are talking about names
20:34 Igloo No, I don't know what it looks like yet, but I'm confident that it's true
20:35 Igloo Well, fairly confident anyway
20:35 Igloo I suspect it'll look largely like your permutivity proof, which I haven't read properly
20:35 Heffalump fair enough. But I still don't really understand the statement. You are defining an ordering on names, based on the dependency of patches with those names. So first you need to prove that makes sense; you claim that your axiom implies that.
20:36 Heffalump Then you need to prove transitivity and anti-symmetry - do you also claim that your axiom implies those?
20:36 Heffalump I'm sure my proof can be done better, it's very long-winded.
20:37 Igloo Do you need anti-symmetry for a partial order?
20:37 Heffalump I hope so!
20:37 Heffalump otehrwise it wouldn't be much of an order
20:37 Heffalump (yes, you do, having checked)
20:38 Igloo Oh, I was misremembering what it said
20:38 Heffalump oh, you also need reflexivity. Which is a bit ugly here.
20:38 Heffalump though perhaps you can define dependency as the <
20:38 Heffalump the reflexive closure of that is what is a poset
20:38 Igloo Right, so it's not quite dependency, it's "in the minimal sequence containing"
20:38 Heffalump no, it should be dependency.
20:38 Heffalump That's much simpler.
20:39 Heffalump I presume the reflexive closure of that equates to "in the minimal sequence containing"
20:39 Heffalump (much simpler to understand, that is)
20:39 Igloo Yeah, they're equivalent
20:39 Heffalump I think you might also need to define dependency as the transitive closure of "commute with the inverse fails".
20:40 Igloo I don't follow
20:40 Igloo In pq, q depends on p if p and q don't commute
20:40 Heffalump well, how do you propose defining it?
20:40 Heffalump and what if pq never exists?
20:40 Heffalump sorry, I didn't mean "with the inverse"
20:40 Igloo Then q doesn't depend on p
20:40 Heffalump I just meant "commute fails".
20:41 Igloo ("directly depend" really)
20:41 Heffalump ok, so then for the poset you *will* need the reflexive transitive closure of "directly depend"
20:41 Igloo Right, yes. It was the inverse bit that confused me
20:41 Heffalump ok. So the only thing actually left to prove is antisymmetry.
20:42 Heffalump which actually seems tricky to me.
20:42 Heffalump unless you have an axiom that pq <-> fail precludes the existence of q'p'
20:42 Heffalump or perhaps that's the point of the "permutitity" axiom.
20:43 Igloo The permutivity axiom says that you can't make it commute by commuting things past it
20:43 Heffalump Hmm. I think you need to explain the consequences of that one rather more.
20:43 Heffalump you need to define a closed universe at some point
20:43 Igloo Yeah, I waffle about it at the start of the Named Patches section, but I'll be more formal in this rewrite
20:43 Heffalump my theory draft has a lot of proofs by induction on the structure of commutation.
20:46 Igloo of catch commute, you mean?
20:47 Heffalump I don't have any catches.
20:47 Heffalump but of patch commute sequences, yes
20:48 Igloo What structure has commutation got, then?
20:49 Heffalump http://urchin.earth.li/darcs/ganesh/​darcs-patch-theory/theory/formal.pdf
20:49 Heffalump the first page defines it
20:50 Igloo Ah, I see, of sequences, not just patches
20:51 Heffalump yes, but that's pretty important
20:52 Heffalump you might come by q'p' without ever commuting p and q. At least you might if you don't set up the axioms so that it's not possible.
22:55 Igloo Heffalump: Hmm, maybe you do need to know that the various ways of getting a patch to a given context give you the same patch
22:57 Igloo Without that I can't see how to show that, if <ab,cd> <-> <c'd',a'b'> than ab commutes iff a'b' does, in the case where you commute the c and d patches while they are between the a and b patches
22:57 * Igloo wonders if that made sense
23:03 Igloo http://urchin.earth.li/~ian/permute.png is what I mean, anyway

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