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'
visually:
+-- 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.
Regards,
apfelmus
--
http://apfelmus.nfshost.com
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
