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

James Cook falsifian at falsifian.org
Sat Dec 12 17:22:32 UTC 2020


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

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

b) The all-zero node is present.

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

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

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

-- 
James


More information about the darcs-users mailing list