[darcs-users] darcs patch theory

Ian Lynagh igloo at earth.li
Wed Sep 17 20:03:45 UTC 2008


On Wed, Sep 17, 2008 at 05:24:24PM +0200, Hubert Kauker wrote:
> 
> first of all I do apologize for having sent html mail before.
> Hope this is better.

Perfect, thanks!

> I think I'm getting slowly what the theory means.

Great! Most of what you said is right, but below I've only responded to
the bits where it's wrong or you've asked questions.

> In axiom (4.2) the "inverse" of a patch comes up.
> So the set P is required to have a neutral element e (see definition 5.1) and the existence of inverses makes P into a group.

e is the empty sequence, not the identity patch.

So P is not required to be a group.

> Patch inversion must be compatible with commutation in this way: [let 1/p denote the inverse of patch p]
> (4.4) When c(p,q) = (r,s) then c(1/r,p) = (s,1/q).
> 
> In section 4 the names of patches come up. What is a "name" ?
> All names obviously form a group N and we have a group homomorphism n:P-->N .

Aha, no. I'll try to make this clearer for the next draft:

Unnamed patches are an input to the paper. For example,
    AddFile "foo"
is an unnamed patch.

Named patches are part of the output of the paper. So a repository might
look like:
    [+"Add foo to the repo"; AddFile "foo"]
    [+"Changed my mind"; RmFile "foo"]
    [+"I was right the first time"; AddFile "foo"]
Here, the things in square brackets are named patches.
The first one has name +"Add foo to the repo" and performs the unnamed
patch (AddFile "foo").

The only thing you can do to names is invert them (change their sign).
You can't join two of them together or anything.

> It follows that p is positive if and only if its inverse is negative.
> What abount mixed compositions of several positive and negatives patches?

You can't compose 2 patches to get another patch. Patch composition is
really patch sequence composition; the confusion is probably because the
patch p and the singleton sequence of patches p look the same in my
notation. Also, I make sequences in explanatory text before I've
formally introduced them.

> One does not really get, what names are used for.

I'll add a bit of blurb.

> A Boolean property "sensible" is introduced on the set of all patch sequences.
> It needs to satisfy certain axioms which I omit here.
> One has no idea (at this point) what the concept is used for.

And yet more blurb  :-)

> At the end of section 5 repository states make their appearance again in the explanations.
> Is a repository state a context?

Yes; will clarify in the doc.

> At the end of section another fundamental definition is made rather quietly.
> Two patch sequences are considered "equal" when a certain condition holds.
> In fact, we have the equivalence relation generated by the commutation relation <--> .
> What happens when during commutation you get a patch and its inverse next to each other? Can you "cancel" them?

No: p inverse(p) is not the same as the empty sequence, as some patches
cannot commute past p inverse(p), but can commute past the empty
sequence.

> Section 6 is informal and describes the "merging of patches".
> Merging of patches is probably the wrong term, because it seems that merging of *patch sequences* is meant.

Ah, I see what you mean. There are two parts to it: There's how to merge
2 patches, giving a patch sequence of length 2; and there's how to merge
two patch sequences using the first merge.

> It begins with two repositories, but we have never said what a repository is.

Right, I should talk about sequences here, not repos.

> It looks as though a repository is a patch sequence.
> What the result of merging?
> Another patch sequence?

Yes, merging patches or sequences of patches give you a patch sequence.

Later on we'll define merge for catches and sequences of catches, which
will give you a sequence of catches.

> It looks as though we start with two patch sequences xq and xr.
> Here x is any patch sequence and q and r and individual patches.
> And juxtaposition  means the natural composition of sequences.
> We then try to find two more patches q’ and r’ such that c(q,r’) = (q’,r) or (q,r’) <--> (q’r).

c(q,r') = (r,q')
or
(q,r') <-> (r,q')

The second diagram in Section 6 should help if this is unclear.
q r' and r q' are the two ways to get from the top to the bottom.

> We then declare the patch sequence (=repository) x(r’.q) as the result of the merge.

x r q'
or
x q r'

There's actually another way to think about merges, that I plan to
describe:

Suppose we have xq and xr. We want to get the effects of both into a
single repo. Then we can make the sequence
    x q inverse(q) r
and then do the commute
    c(inverse(q),r) = (r', inverse(q)')
giving us
    x q r' inverse(q)'
and then just throw away inverse(q)'
    x q r'

I think this way is easier to understand at first, but the other way is
easier once conflictors get involved.

> It is good to make an effort and base darcs development on a sound logical foundation.
> Thanks again for making available early drafts of the theory.

Thanks for your comments and encouragement!

> There is great potential there, but understandably also great need for streamlining.

Yes; when I started I didn't even know what the axioms, algorithms etc
were going to be, let alone the best way to present them  :-)

Hopefully things are settling down now, though...


Thanks
Ian



More information about the darcs-users mailing list