[darcs-users] Patch Theory in action

Marnix Klooster 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:

  C(B(A(e)))

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:

  y
=   "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"
  z

> 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 
> patches.
> 
> Whew.

Again for what it's worth: here is a proposal for an alternative
notation.

 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
            have.]
 def(<an expression resulting in a tree>) : the result of the
                                            expression is
                                            defined
     [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
this domain.

Groetjes,
 <><
Marnix
--
Marnix Klooster
mklooster at baan.nl <mailto:mklooster at baan.nl> 




More information about the darcs-users mailing list