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

James Cook falsifian at falsifian.org
Fri Dec 11 23:13:19 UTC 2020


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

I think something like that would work. I don't think describing it as
a "subgroup" works exactly. For one thing, the elements of the set are
sequences of names, which are not themselves permutations. You could
pick one "canonical" ordering and identify each other sequence with the
permutation that re-orders the canonical ordering into it, so at least
you have a set of permutations, but I don't know if it will be a
subgroup.

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

Here are three more attempts. Not necessarily better than yours, but
maybe food for thought.

1.

I suspect the following two properties together may be equivalent to
(a fixed-up version of) your permutation-subgroup property:

a) name(pq') = name(p) U name(q) whenever pq' is a clean merge of p and
   q (defining a clean merge as a pushout, as before).

b) Rule out this diagram:

> >       *
> >     a/ \b
> >     /   \
> >    *     *
> >  d/|c  c'|\d'
> >  / |     | \
> > *  *     *  *
> > |   \   /   |
> > |  b'\ /a'  |
> > |     *     |
> >  \         /
> >   \       /
> > b''\     /a''
> >     \   /
> >      \ /
> >       *

by saying that for every commuting square

   *
 a/ \b
 /   \
*     *
 \   /
  \ /
   *

the pushout (clean merge) of a and b exists.

I haven't fully worked out a proof that (a) and (b) is equivalent to
something about transpositions, but it seems likely to be true. Maybe I
should think about it more.

2.

This is a more radical change, so I'll start from the beginning.

A patch theory consists of:

* a set N of names, and

* a set C of sets of names (i.e. C is a subset of the powerset of N)
  (elements of C are called "contexts")

such that C contains the empty set, and for any c1, c2, c3 in C, if
c1 ⊆ c3 and c2 ⊆ c3, then c1 ∪ c2 is an element of C.

That's all. But we need to connect this to more familiar terms...

If we like, we can view this as a category using the order relation ⊆.
Specifically: the objects are contexts, and there is a single morphism
from c1 to c2 if c1 ⊆ c2, otherwise none.

A "patch" is just a morphism between two contexts that differ by the
inclusion of one name.

This is similar to your category view. The difference is that patch
sequences can no longer represented as morphisms (unless you're willing
to forget the order). Of course this doesn't prevent us from talking
about patch sequences.

3.

#3 is just a rephrasing of 2 to be more compatible with your
categorical point of view.

Define N and C as in 2 above (including the requirements I imposed on
C).

Define a graph G as follows. The nodes are all elements of C. The edges
are all pairs (c1, c2) where c2 and c1 differ by the inclusion of one
name (c2 = c1 ∪ {n}); the edge is labelled by that name n.

Define the free category on G as in your original formulation. Note
that the name of any path will just be the set difference of its
endpoints, so your requirement that parallel paths have the same name
is satisfied. The additional requirements on the set C (taken from #2)
will hopefully ensure that clean merges behave well.

-- 
James


More information about the darcs-users mailing list