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

[Jason Dagit]

On Thu, Oct 29, 2009 at 10:38 AM, Heinrich Apfelmus <
apfelmus at quantentunnel.de> wrote:

> 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
>

David and I would use the term parallel here.  Others might prefer
concurrent.  I just needed to make it more precise.


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


I think we should think about the state of the repository.  We take as an
assumption (axiom?) that context defines the state of the pristine.  Two
equal states could result from different contexts, but two 'equivalent'
contexts always define the same state.  Here equivalence is defined in terms
of sequences that can be reordered under commute. What has never been
formally verified is that commute does actually act as an equivalence
relation in this sense.  I give the details of what needs to be verified in
my MS thesis, which can be downloaded from here, look at Chapter 3:
http://ir.library.oregonstate.edu/jspui/handle/1957/11180

Getting back to the intuition, given the setup we have where things 'commute
nicely', then I expect you can make a proof or disproof of this
'permutivity' by looking at the state transformations.  Similar to the
intuitive argument I made in my previous email.  Try reasoning about what it
means to apply the transformation in a particular state.

How can X and Y combine to create something that conflicts with the
transformation represented by Z?  I'm sort of rushing here as I don't have a
lot of time to dedicate to this right now.  Perhaps can you construct a
proof either way?

Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20091029/19610de2/attachment.htm>