[darcs-users] Write-up on "tree repositories" as an alternative to conflictors

[Ben Franksen]

Am 05.12.20 um 00:09 schrieb James Cook:
> On Thu, Nov 26, 2020 at 02:12:56PM +0100, Ben Franksen wrote:
>> I would start the whole thing with a slightly different definition.
> 
> This seems like a nice way to do things. I like the reuse of terms from
> category theory.
> 
> Do you happen to know how much this has in common with "A Categorical
> Theory of Patches" which pijul is based on? I have not read the paper
> in detail, but I know they too talk about pushouts.
> https://arxiv.org/abs/1311.3903

I don't think it has a lot to do with it, apart from the idea to define
clean merges as pushouts (which is indeed quite an obvious idea, once
you realize that patch sequences form a category). The paper asks (and
answers) the question "what would be the minimal extension of the
category of file contents (lists of lines/tokens) and atomic changes
(insert a line at given pos, remove a line at given pos), such that all
pushouts exist in it?" This is about (a certain class of) primitive
patches, whereas our discussion is about abstract patch theory.

>> We extend the three functions above to paths. The source of a path is
>> the source of its first patch, the target is the target of its last
>> patch, and the name of a path is the set of names of its patches:
>>   name(p1,...,pn)={name(p1),...,name(pn)}
>>
>> This is indeed an extension if we identfy a name with the singleton set
>> consisting of just that name.
> 
> nit: The empty patch has no patches, so these definitions of source and
> target don't work for it.

Right, that was sloppy. Indeed this should serve to remind us that there
are lots of /different/ "empty sequences" (namely one for each context).

>> We can define the clean merge of two paths as follows. Let p and q be
>> paths with the same source. A clean merge of (p,q) is a then a pushout,
>> in other words, another pair of paths (q',p'), such that pq' and qp' are
>> parallel, and such that q',p' are minimal in the sense that for any
>> other such pair (q'', p'') there is a unique path r such that q'',p''
>> factors through r; that is, p''=p'r and q''=q'r. It follows from the
>> defining property of a patch theory that name(pq')=name(qp'), but I
>> think it should also be possible to deduce
>>
>>   name(pq') = name(p) U name(q)
>>
>> using the universal property (minimality) of the merge. Indeed I think
>> both definitions are equivalent. Note that any such merge must
>> necessarily be unique (because pushouts are unique).
> 
> I think the following is a counterexample. Suppose this is the whole
> patch theory. All edges go downward. a and a' have the same name and so
> do b and b' and c and c'.
> 
>    *
>  a/ \b
>  /   \
> *     *
> |c    |c'
> |     |
> *     *
>  \   /
> b'\ /a'
>    *
> 
> In this case, the pushout of a and b is the whole diagram, so the merge
> is acb' or bca', both of which include c's name.

You are right. Such a scenario must not be allowed and the "global"
definition of patch graph I gave is too weak to exclude it. If you
analyse the counter example from the POV of permutations of names, what
we have here is (indeed the simplest example of) a permutation group
that is not generated by adjacent transpositions. If we build a patch
theory bottom-up starting with commutation of single patches, then this
cannot happen: the set of parallel paths from s to t always maps to a
permutation group that is generated by adjacent transpositions.

So one way to "fix" the theory could be to add that as a requirement.
Formally, consider the map from paths to sequences of names. For each
pair (s,t) of contexts, the image of the set of parallel paths from s to
t under this map can be regarded as a subset of S_N (where N is the
common path length). The requirement is that this is a subgroup
generated by adjacent transpoisitions.)

At least I *think* that would fix the theory, i.e. allow to prove my
conjectures about merges. However, it feels a bit heavy-weight and I
would prefer a more elegant way to express this requirement.

> Maybe an axiom could be added that name(pq') = name(p) U name(q)
> whenever pq is a clean merge of p and q. I suspect it is strictly
> weaker than my Assumption 4.1 but it is more succinct and maybe it is
> enough.
> 
> (The example violates Assumption 4.1: conflict(a, b) must be true
> because a and b can't be merged directly, but then the paths acb' and
> bca' contain conflicting patches, which is not allowed. Maybe this can
> be turned into a proof.)
> 
> Here's an example showing the name union axiom doesn't imply 4.1:
> 
>       *
>     a/ \b
>     /   \
>    *     *
>  d/|c  c'|\d'
>  / |     | \
> *  *     *  *
> |   \   /   |
> |  b'\ /a'  |
> |     *     |
>  \         /
>   \       /
> b''\     /a''
>     \   /
>      \ /
>       *
> 
> Now there is no pushout of a and b, so the name union axiom has nothing
> to say, but 4.1 is still violated.

Yes, this doesn't surprise me. The above would of course be excluded by
the (somewhat crude) fix I proposed above.

Cheers
Ben