[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)
apfelmus at quantentunnel.de
Thu Oct 29 17:38:44 UTC 2009
Jason Dagit wrote:
> Heinrich Apfelmus wrote:
>> My amusing (to me) observation was that this "intuitively correct"
>> property is equivalent to the following property about merges:
>> Consider three concurrent patches
>> X = C^(-1) inverse of C
>> Y = A
>> Z = B'
>> +-- X +-- C --<
>> | |
>> >---+-- Y <=> +-- A (-- B)
>> | |
>> +-- Z +-- B'
>> X Y Z concurrent <=> C A B in sequence
>> such that
>> X and Y can be merged (i.e. X and Y^(-1) commute)
>> Y and Z can be merged (...)
>> Z and X can be merged (...)
> I don't understand the setup of this example. What does it mean
> for two or more patches to be concurrent? Also, the notation for
> your diagram is unfamiliar so I need an explanation of the symbols
> (>--) vs. (--<), (-- B), what does + represent, etc. At first I
> thought it was an ASCII art tree, but if that is true why do you
> say C A B is a sequence when they appear to branch from the same
> level of the tree? And I think you might have more than one
> notation for inverses, C^(-1) vs. (--B).
> Do you think it would help if we used the context notation here?
Yes, I didn't intend to cloud the issue with my botched ASCII art;
let's use context notation.
> For example, this is what I think you mean:
> oXx, oYy, oZz, would mean that X, Y, and Z all have the same pre-
> context (meaning they all apply to the same sequence of patches).
> and you have, iCcAaBb as a sequence. So then, I think you mean to
> commute A and B so that we get cB'd.
> In this notation the lower case letters represent the context of
> the patches. The context before the patch is the pre-context and
> it is where the patch applies, similar to the domain of a function.
> The post-context is the resulting context from applying the patch
> (so, c = i with C on the end). When patches are in a sequence we
> omit the contexts that are implied or redundant.
Ok, so the situation is indeed the following: we have three parallel
(concurrent? what's the established name?) patches
o X x, o Y y and o Z z
and want to merge them. (I'm separating contexts and patches by
spaces as this will make better notation subsequently). Now, we
assume that each pair can be merged, i.e. we have
x X^(-1) o Y y <-> x Y1 xy X2 y
y Y^(-1) o Z z <-> y Z1 yz Y2 z
z Z^(-1) o X x <-> z X1 zx Z2 x
so that we can build for example the repositories
o X x Y1 xy (X and Y merged)
o Y y Z1 yz (Y and Z merged)
o Z z X1 zx (Z and X merged)
Is this enough to establish the existence of a patch xy Z' xyz that
merges Z into the union of X and Y, i.e. that allows us to build o X
x Y1 xy Z' xyz ?
No, I think the three premises are not enough. This has to be a new
axiom or a consequence of other axioms. It does look like
permutivity, but as I understand it, permutivity makes the existence
of Z' a premise, not a consequence.
More information about the darcs-users