[darcs-users] Simple commutation theorems
droundy at abridgegame.org
Wed Nov 26 12:17:13 UTC 2003
On Tue, Nov 25, 2003 at 08:42:05PM +0100, Marnix Klooster wrote:
> 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.
I just realized that I misread your condition, which was that
P;Q << Q
which implies that P;Q is valid. I was thinking the condition was P << Q,
in which case my objection would have made sense.
> 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...
There are two difficulties with this approach. One is simplifying -Q;P;Q
and the other is figuring out a compact way to evaluate the << relation.
For simple cases << is easy, but thinking beyond 1.0, it will probably get
more difficult (since I hope to add more interesting patch types, such as
word-based diffs). On the other hand, the commutation function will be
getting more difficult as well, so it's not obvious which will be easier.
Simplifying -Q;P;Q seems likely to be the major problem. Currently, my
approach to simplifying this would be to commute -Q;P and then use the fact
that -Q;Q = 1 (identity). But that wouldn't gain us anything, since the
whole point is to simplify implementation of the commute.
Implementing both the << and the simplify as a replacement for commute
seems unlikely to be simpler than implementing a commute.
On the other hand, your theorems suggest an interesting possibility: is it
always the case that when two patches are commuted, one of them is
unmodified? i.e. given two commuting patches P;Q, must it be true that
either (P;Q << Q) or (P;Q << P;Q;-P) ? I've been unable to think of a
counterexample, but of course that doesn't prove anything. I have some
intuitive feeling that you'd run into a consistency problem if you had
P;Q commutes to Q';P' where P /= P' and Q /= Q'
but I'm not sure what the consistency problem would be. If we can prove
that one of the patches is unmodified in a commute, it would remind me of
something like a Kramers-Kronig relation (which is the relationship in the
frequency domain caused by causality constraints in the time domain). By
(possibly horridly flawed) analogy to the usefulness of Kramers-Kronig, I
speculate that this patch conjecture could be very useful.
To clarify the conjecture, it is that
if P;Q commute then
either P;Q commutes to Q';P
or P;Q commutes to Q;P'
By your theorem above (and a bit of simplifying) we could rewrite this to
if P;Q commute then
either P;Q << Q
or -(P;Q) << -P
If nothing else, such a theorem would provide a convenient means of
categorizing commutation rules by writing an asymmetrical commutation
function that only deals with one of the two cases and then trying it on
both P;Q and -(P;Q). I already do something like this, but using a
symmetrical commutation, which may lead to specifying the same case twice.
More information about the darcs-users