[darcs-users] Simple commutation theorems
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".
More information about the darcs-users