[darcs-users] Simple commutation theorems

Marnix Klooster mklooster at baan.nl
Mon Nov 24 08:47:35 UTC 2003


Hi all,

This weekend I figured out two rules that might make the implementation of
commutation easier, since (if I understand the source code correctly) a lot
of special cases that are coded out separately can now be treated more
generally.

(But will perhaps be replace by other special cases; see below.)

I'm using the notation I proposed earlier, for ease-of-ASCII-typing; so
patchs lists are written left-to-right.

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

    T;P;Q
  =   "allowed because def(T;Q); see below"
    T;(Q;-Q);P;Q
  =   "move brackets"
    T;Q;(-Q;P;Q)

So P;Q = Q;(-Q;P;Q).  Since Q is the same patch as Q, and P
is (do some hand-waving here) 'the same change as' -Q;P;Q,
(P,Q) commutes with (Q,-Q;P;Q).

Note that T=T;Q;-Q only holds when patch Q is applicable to T,
so when def(T;Q).  This is the case when P;Q << Q:

     def(T;Q)
  <=   "definition of P;Q << Q"
     def(T;P;Q)
  ==   "given"
     true

(End of Proof.)

What does this mean for the implementation?  It means that many
cases of the commutation code can be replaced by a perhaps simpler
implementation of the '<<' operator, perhaps supported by code
that simplified patches like -Q;P;Q.

I don't know whether this really helps.  I just thought I'd post this.

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




More information about the darcs-users mailing list