[prev in list] [next in list] [prev in thread] [next in thread] 

List:       darcs-users
Subject:    Re: [darcs-users] How to extend a patch theory to fully commute
From:       Ben Franksen <ben.franksen () online ! de>
Date:       2020-07-07 9:08:48
Message-ID: re1e30$m3t$1 () ciao ! gmane ! io
[Download RAW message or body]

Definition: A category X is said to be an inverse category whenever, for
each arrow f : A -> B in X, there exists a unique f^ : B -> A in X such
that ff^f = f and f^ff^ = f^.

(I write composition as juxtaposition without an operator.)

Given a universe of extended invertible patches, define a category as
follows:

 * Objects are the extended contexts.
 * Arrows are (finite) sequences of extended patches, with the
   identifications pp^p = p and p^pp^ = p^ and pq=q'p' whenever
   commute(pq)=q'p' (which I also write as pq<->q'p')
 * Composition is concatenation.
 * Identities are empty sequences (denoted id_X : X -> X).

In other words, we start with the free inverse category on the graph of
extended patches and factor that by the equivalence relation that
identifies sequences that differ only up to commutation. This is also an
inverse category because commutation respects inversion i.e.

  pq<->q'p' <=> q^p^<->q'^p'^,

which is a consequence of the square-commute law.

Some remarks:

 * I think in your theory you need to show that the squere-commute law
   holds for extended patches (assuming it does for primitive patches).

 * This construction works only if extended patches do have inverses
   i.e. not for Darcs. In Darcs we give up invertibility when we extend
   primitive patches, and instead define merging as a new "primitive"
   (sorry for overloading the term) operation. In your definition of
   extended patches invertibility falls out quite naturally, and indeed
   is required because you define merging in terms of inversion as in
   the primitive theory.

So our arrows are equivalence classes of extended patch sequences. The
construction is such that given a sequence P=...pp^p... we can reduce
that to an equivalent smaller P'=...p... and I think it should be
possible to show that all members of a class that are minimal (with
respect to the length of the sequence) have the property that any patch
they contain occurs at most once. (Formally: if names(P) is the set of
names of patches occurring in P, then |names(P)|=length(P).)

It is assumed that the primitive patch graph has a distinguished node
(context) O that denotes an empty state with no files or directories.
Since primitive contexts are embedded in extended contexts, we could
then define a repository as an arrow in the inverse category of extended
patch sequences that starts at O.

Cheers
Ben

_______________________________________________
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users
[prev in list] [next in list] [prev in thread] [next in thread]