[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)

[Heinrich Apfelmus]

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