Time 
Nick 
Message 
08:17 

kowey joined #darcstheory 
12:57 

kowey joined #darcstheory 
16:55 

arjanb joined #darcstheory 
19:38 

kowey joined #darcstheory 
19:56 
Heffalump 
Igloo: I've had a bit of a look at camptheory 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 nway 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 nway 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 nway 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 iforonlyif 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 3way 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 antisymmetry  do you also claim that your axiom implies those? 
20:36 
Heffalump 
I'm sure my proof can be done better, it's very longwinded. 
20:37 
Igloo 
Do you need antisymmetry 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/darcspatchtheory/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 