[darcs-users] Simple commutation theorems

David Roundy droundy at jdj5.mit.edu
Mon Nov 24 11:57:58 UTC 2003

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".
David Roundy

More information about the darcs-users mailing list