[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