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

James Cook falsifian at falsifian.org
Fri Dec 4 23:09:02 UTC 2020


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

Maybe I should move my patch trees write-up to a separate document so
the old "Patch universes" stuff can stay where it is without getting in
the way.

A couple of comments below:

> 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.

> 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.

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.

> Cheers
> Ben

-- 
James


More information about the darcs-users mailing list