Re: Why darcs? What does the 'physicists proof' actually prove?

On Wednesday, July 23, 2003, at 09:27  PM, David Roundy wrote:

> Just one more thought I had on the differences between VAP and darcs.  
> That
> is that if you don't view the commute as a fundamental operation, you 
> are
> likely to lose the benefit of a number of the properties that darcs 
> has.
> For example, because
>
> A || B => A'B <---> B'A
>
> the order in which you perform the merge doesn't matter.  If your merge
> doesn't have this property then the merge theorem doesn't apply and the
> VAP(inv(A),B) method of doing a commute may be irreversible--it would
> depend on what constraints you did place on the VAP function.

I guess an equivalent restriction on VAP would be:

VAP(A, B).A <--> VAP(B, A).B

In the absence of conflicts, I believe this holds for the VAP function 
(although I haven't proved it formally or anything :).  When conflicts 
exist, VAP is a little less well defined -- it states that the user 
resolves the conflict.

I would also expect that VAP(Inv(A), VAP(A, B)) <--> B, again in the 
absence of conflicts.  This is the VAP equivalent of the statement that 
two commutes gets you back where you started.

> > Theorem 2 states that P2'.P1 <-> P1'.P2 iff Inv(P1').P2' <-> 
> > P2.Inv(P1)
> >  (assuming everything is actually calculable).
> >
> > This tells us when certain things commute.  In addition, we know P2 
> > and
> > Inv(P1) and can hence get Inv(P1').P2'.
>
> I would say rather that this tells us when certain patches 
> merge--without
> conflict, that is.

Ahhh.  With VAP, the VAP function detects conflicts (where in darcs, 
commute is used to detect conflicts).

> > But, how do you get Inv(P1') and/or P2' from Inv(P1').P2'?  What tells
> > us how to break this patch apart?
>
> The key thing here is that commute is a function that takes two inputs 
> and
> give two outputs (as it must, in order to be useful).  So when you 
> commute
> P2 and Inv(P1) we get out Inv(P1') and P2' already broken apart.  The
> "multiplication" notation is just intended to make clear the 
> relationship
> between the two patches.

This is a key point I was missing.  Thank you for setting me straight.  
That makes everything much clearer.

> So to summarize, Theorem 2 tells us (with regard to merging--it also 
> has
> other uses) how to take a commutation function and turn it into a merge
> function.  This is very cool, because commutation has more and simpler
> properties than the merge does.  Most importantly, commutation is a
> self-inverse function--commute twice and you get back the same result.
> Also, the composed commuted patches must be equivalent to the original
> composed patches.

At this point it is looking more and more to me that VAP and darcs are 
equivalent in the absence of conflicts.  I don't understand darcs 
behaviour in the presence of conflicts well enough to say more.

VAP uses the darcs concept of merge as the fundamental operation, and 
derives commute.  darcs uses commute as the fundamental operation and 
derives merge.

Again, thanks for taking the time to describe this in detail.

Will         :-}

--
Dr William Uther                            National ICT Australia
Phone: +61 2 9385 6926             School of Computer Science and 
Engineering
Email: willu@xxxxxxxxxxxxxxx             University of New South Wales
Jabber: willu@xxxxxxxxxxxxxxxxxxxxxx          Sydney, Australia