7.19 Non-Commuting Operators

An operator can be declared to be non-commutative under multiplication by the declaration NONCOM.


After the declaration

  noncom u,v;

the expressions u(x)*u(y)-u(y)*u(x) and u(x)*v(y)-v(y)*u(x) will remain unchanged on simplification, and in particular will not simplify to zero.

Note that it is the operator (U and V in the above example) and not the variable that has the non-commutative property.

The LET statement may be used to introduce rules of evaluation for such operators. In particular, the boolean operator ORDP is useful for introducing an ordering on such expressions.


The rule

        for all x,y such that x neq y and ordp(x,y)  
           let u(x)*u(y)= u(y)*u(x)+comm(x,y);

would introduce the commutator of u(x) and u(y) for all X and Y. Note that since ordp(x,x) is true, the equality check is necessary in the degenerate case to avoid a circular loop in the rule.