[darcs-users] Simple commutation theorems

[David Roundy]

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
say that

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.
-- 
David Roundy
http://www.abridgegame.org