[darcs-users] Patch Theory in action
mklooster at baan.nl
Sat Nov 22 20:29:56 UTC 2003
Kevin Smith wrote (in part):
> While on the subject of the manual, I found a couple other things in
> Appendix A hard to follow:
> 1. Why are the patch lists "backward"? I expect ABC to mean that patch A
> was applied first, not last.
The reason is that David is a physicist, and thinks in an analogy to
quantum physics. Every patch is an 'operator'. The same would
probably be true for mathematicians (like me), who would view a patch
as a 'function' mapping a tree to a(nother) tree. For example,
applying A, B, and C to the empty tree e, in that order, can be
written as follows:
or (using 'o' for function composition)
(C o B o A)(e)
(See also point 4, and my notation proposal below.)
> 2. The M(A, B) notation is never mapped back to the ABC notation, which
> seemed jarring.
I agree that this notation is confusing, because (I think) M(A,B) is
used both to mean 'the change that results by merging changes A and B'
and 'the patch that results by merging changes A and B'. I think that
the Theory description will be a lot clearer when the patch/change
distinction is strictly kept.
In a similar way I find the notation
P1 || P2 ===> ... <--> ...
confusing. I think that I know what is meant, but as a mathematician
this is too semi-formal to make formal sense.
> 3. The statement "it is possible to show that the right inverse of a
> patch is equal to its left inverse." is never really explained. What is
> a "left inverse" or a "right inverse"?
A little group theory. In general, assume that we have a set S (say,
of patches), and an operator (say, o) that takes two elements of S and
produces a(nother) element of S. The operator is associative:
x o (y o z) = (x o y) o z
Also assume that S has an identity element i for which
x o i = i
i o x = i
holds. Now, a left inverse of x is a y such that
y o x = i
and a right inverse of x is a z such that
x o z = i
If we now have an x, y, and z for which the above holds (so: x has
some left inverse y and some right inverse z), then y=z:
= "i is the identity element"
y o i
= "z is a right inverse of x"
y o (x o z)
= "o is associative"
(y o x) o z
= "y is a left inverse of x"
i o z
= "i is the identity element"
> 4. I found this statement (immediately after Theorem 2) difficult to
> follow "This can easily be proven by multiplying both sides of the first
> commutation by * on the left, and by * on the right." As a programmer
> (not a mathematician), the idea of "multiplying" patches seems odd.
[snipped clarified proof of Theorem 2]
In the notation introduced above, "multiply by P3 on the right" means
to do the following step:
P1 = P2 => P1 o P3 = P2 o P3
> If ABC meant to do patch A first (instead of last), then this wording
> could use "beginning" and "end", because they would refer both to the
> symbolic representation, and to the chronological application of the
Again for what it's worth: here is a proposal for an alternative
e (or Greek epsilon) : the empty tree
T,T1,T2 : some arbitrary tree, usually used as a 'context'
T1 = T2 : T1 and T2 are exactly the same tree.
P,P1,P2,Q,Q1,Q2 : arbitrary patches (mathematically these are
partial functions from trees to trees)
[NOTE: Personally I rather dislike primes (e.g. in P'') to
create new related variable names; I like numbering
better. So P1 and P2 would usually denote two
patches representing the same change.]
P = Q : P and Q are exactly the same patch: for every tree
they either both are inapplicable, or they both
give the same result tree.
[NOTE: So commutation would be written as P1;Q1 = Q2;P2;
see the following notation.]
T;P : the tree after applying patch P to tree T
[NOTE: This solves the order problem that Kevin and I
def(<an expression resulting in a tree>) : the result of the
[Example: If P is "rename file F to G", it can only be
applied to all trees containing a file named
F. So def(T;P) is true for every T that
contains such a file, and false otherwise.]
P;Q : the patch such that for every T, (T;P);Q = T;(P;Q)
[NOTE: This double use of ; creates a syntactic
ambiguity, but not a semantic one, because
by definition both interpretations of T;P;Q
are the same.]
-P : the inverse of patch P, i.e., for every T for which
def(T;P), we have T;P;-P = T.
[NOTE: Personally I dislike superscripts and subscripts.]
P || Q : P and Q apply to the same set trees: for
every T, def(T;P) == def(T;Q)
I don't have time to work this out further now, or give examples. But
I agree with Kevin that a left-to-right notation is more intuitive for
mklooster at baan.nl <mailto:mklooster at baan.nl>
More information about the darcs-users