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

[Ben Franksen]

Am 12.12.20 um 18:22 schrieb James Cook:
> On Sat, Dec 12, 2020 at 02:32:07PM +0100, Ben Franksen wrote:
>> Am 12.12.20 um 11:56 schrieb Ben Franksen:
>>> Another aspect not covered is that for permutivity to hold, we need not
>>> only ensure a /minimum/ number of parallel paths, but also a /maximum/
>>> number of intermediate contexts. The extreme case is the commuting
>>> hypercube of dimension n with n! different paths of length n (all
>>> permutations of n), sharing 2^n contexts (the corners of the hypercube).
>>
>> Indeed, it should be possible to embed (inject) any patch graph into an
>> N-dimensional hypercube, where N is the set of natural numbers. I find
>> this view quite illuminating.
>>
>> (We have to restrict names and contexts to (at most) countable sets,
>> which is not a serious limitation, since this will be the case in any
>> practical implementation anyway.)
>>
>> The contexts correspond to corners i.e. elements of {0,1}^N, and the
>> patches correspond to edges. Edges representing patches are considered
>> directed "away from the origin". The names are the (mutually orthogonal)
>> "directions" in our space: two patches have the same name if and only if
>> they are /geometrically/ parallel as edges.
>>
>> We even get a distinguished "empty context" for free (the origin).
>>
>> Corners can be seen as sequences of bits (with only finitely many 1s),
>> and a patch p:s->t with name m corresponds to the triple (s,t,m) where
>> s(m)=0, t(m)=1, and s(i)=t(i) for all names i with i/=m.
> 
> This is similar to my attempt #2 from yesterday's email (in that
> formulation, a context is a set of names, which could be thought of as
> an element of {0,1}^N if you prefer).

Ah, yes. I didn't understand it in your formulation at first, but of
course this is fully equivalent. Indeed, a context is uniquely
characterised by the names of any sequence of patches that leads up to
it, from the origin i.e. empty context.

>> Given two arbitrary corners s and t, all paths p:s->t must have the same
>> length n, which coincides with the size of name(p). In other words, they
>> lie inside a finite n-dimensional hyperface of the full N-cube.
>>
>> What does permutivity mean in this picture? Or asked differently, how
>> can we characterize the valid patch graphs as a subset of the N-cube?
>>
>> Cheers
>> Ben
> 
> Translating my attempt #2 to these terms, I propose this
> characterization:
> 
> a) First, we only use a subset of the nodes of the hypercube. Each node
>    is either "present" or not. (Think of a "not present" node as
>    representing a set of names with at least one conflict.)

I find the term "corner" more suggestive than "node". But yes.

> b) The all-zero node is present.

Yes.

> c) An edge/patch exists iff its start and end nodes are present.

Yes. Very nice simplification.

> d) If nodes c1, c2, c3 are present, and c1 ⊆ c3 and c2 ⊆ c3, then
>    c1 ∪ c2 is also present.

Interesting! So corners (potential contexts) have an inherent partial
order, indeed they form a join-semilattice. You postulate that if two
contexts have an uppper bound that is also a context, then the minimal
upper bound must also be a context. I think the math term would be that
contexts form a sub-semilattice of the corners.

It's funny how this brings us all the way back to the ideas in your
first paper: instead of focusing on patches or paths, we now focus
almost completely on contexts. And that makes a lot of sense, since
parallel paths are supposed to be "equivalent" anyway. It shouldn't make
a difference *how* exactly we arrive at a context, as long as there is
*any* path that ends there.

And if we thus identify a context c with the set of (equivalent) paths
from the origin to c, then axiom (d) gives us the existence of a clean
merge of two contexts/repos, at least if we know that someone somewhere
has a repo cointaining both our patches.

> For example, I think we can prove the following property from your
> previous email:
> 
>   [for any parallel paths p and q] for every n in name(p)=name(q), and
>   for each i in pos(p,n)..pos(q,n), there exists a parallel path r,
>   such that i=pos(r,n).
> 
> Proof:
> 
> Without loss of generality, assume pos(p,n) <= pos(q,n).
> 
> Write p = p0 a p1 and q = q0 a' q1 where name(a) = name(a') = n. So
> length(p0) = pos(p,n) and length(q0) = pos(q,n).
> 
> Let q0' be a prefix of q0 such that |name(q0') ∪ name(p0)| = pos(q,n).
> 
> Let X = name(q0') ∪ name(p0). By property (d), node X is present in the
> patch theory (taking c1 = end(q0'), c2 = end(p0), c3 = end(p) = end(q).
> 
> X ∪ {n} is also present, again by property (d) (taking c1 = end(q0') ∪
> {n}, c2 = end(p0) ∪ {n}, c3 = end(p) = end(q)).
> 
> By Lemma 1 (below) there exists a path from start(p) to X, and also a
> path from X ∪ {n} to end(p). By property (c), there's also an edge from
> X to X ∪ {n} (with name n). Concatenate these three to get the desired path.
> 
> QED
> 
> Lemma 1
> 
> If the nodes/contexts c and d are present and c ⊆ d, there is a path
> from c to d.
> 
> Proof
> 
> If c = d, take the empty path.
> 
> Otherwise, let n be any name in d \ c. By property (d), taking c1 = c,
> c2 = c ∪ {n} and c3 = d, the node c ∪ {n} is present.
> 
> By property (c), there is an edge from c to c ∪ {n}. Use that as the
> first edge of the path. Note that c ∪ {n} ⊆ d; we can apply the lemma
> again (using induction) to complete the path.
> 
> QED

Nice!

However, remember your counter example of a patch universe with only two
paths with names abc and cba. From the presence of both {a} and {c} we
can deduce that of {a,c}, but it seems impossible to prove that {b} is
present. For that we need a fifth axiom (e) analogous to (d) but with
intersections instead of unions:

e) If nodes c1 and c2 are present, then c1 ∩ c2 is also present.

This means that the (present) contexts must be a sublattice of the
corners. In the counter example, the existence of {a,b} and {c,b} then
imply the existence of {b} and therefore of the full 3-cube.

Note that our lattice of (present) contexts has a bottom element (the
empty context) but no top element (unless the set of names is finite),
which makes formulating (e) easier than (d).

Cheers
Ben