[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