[darcs-users] Simple commutation theorems

[Marnix Klooster]

David Roundy [mailto:droundy at jdj5.mit.edu] wrote:
> On Mon, Nov 24, 2003 at 09:47:35AM +0100, Marnix Klooster wrote:
> > I need to introduce one new concept/notation:
> > 
> >   P << Q == 'for every tree T,
> >              if P is applicable then Q is applicable as well'
> > 
> > Or in other words, the 'domain of P' (the set of trees to which
> > it applies) is subset-or-equal of the domain of Q.
> > 
> > The rules I found are
> > 
> >   P;Q << Q  =>  (P, Q) commutes with (Q, -Q;P;Q)
> >      ...    =>  (P, Q) commutes with (P;Q;-P, P)
> > 
> > I haven't figured out the precondition for the second rule yet.
> > 
> > Proof of the first rule.  For every tree T for which def(T;P;Q),
> 
> It looks like there is a problem here.  What if there is no tree T, for
> which def(T;P;Q)? As I read your << definition, there doesn't seem to be
> any stipulation that P;Q is applicable to any tree.  A simple example for
> which P << Q but P;Q is invalid would be if both P and Q are "rm foo".

I see no problem in this case.  First, if there is no T for which
def(T;P;Q), then P;Q together are the 'zero patch': the patch that is
applicable to no tree.  In that case therefore, the resulting
combination Q;(-Q;P;Q) is also the 'zero patch'.  So from the first
rule above we conclude that ("rm foo","rm foo") commutes with ("rm
foo","zero patch").  That is not really helpful, but it doesn't break
anything either.

What I mean to say is, if we start with a P and a Q that shouldn't be
used in sequence, we end up with two commuted patches that shouldn't
be used in sequence either.

The above rules should be used to commute patches in a correct
repository, where the patches are ordered so that no two patches P;Q
are the "zero patch".  In other cases they work, but they don't help.

By the way, I figured out the precondition for the second rule:

  P;Q << Q       =>  (P, Q) commutes with (Q, -Q;P;Q)
  P;Q << P;Q;-P  =>  (P, Q) commutes with (P;Q;-P, P)

Also, I've been thinking how this could be used in the implementation
(after 1.0, obviously :-).  If you had a Haskell representation of
'the domain of a patch' (when viewing it as a partial function from
trees to trees) --so a description of the set of trees to which the
patch applies-- then it should be fairly easy to compute that domain
for every patch, and also to evaluate the << relation.  Then you can
first check the preconditions of the above rules.  If one of them
works, then compute and simplify either -Q;P;Q or P;Q;-P, and we have
our commutation.

It sounds fairly complex, but I'm curious whether the implementation
would be-- and how this would perform...

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