Commutation Rule

Issue #22 wontfix
created an issue

I don't know if I would call this a proposal, an enhancement, a bug, or simply my misunderstanding of the language. Hopefully, someone can clarify. When working with different algebras it is convenient, to have a commutation rule namely

op a b = op b a;

which is equivalent to

(op a b) - (op b a) = 0;

In some cases, it is an anti-commutation rule namely

op a b = - op b a;

which is equivalent to

(op a b) - (- op b a) = 0;

or more simply

(op a b) + (op b a) = 0;

Sometimes the commutation rule is less trivial and one may have either of the following

(op a b) - (op b a) = ?; (op a b) + (op b a) = ?;

where the question marks are arbitrary. I have tried implementing both commutation and anti-commutation rules (even though this is generally redundant if it is known that a-(-b) = a+b) above for simple multiplication namely

(ab) - (ba) = 0; (ab) + (ba) = 2ab;

In addition, I used the following rules for multiplication namely distributivity of multiplication over addition and associativity of multiplication and addition.

(a+b)c = ac+bc; a(b+c) = ab+ac; a(bc) = (ab)c; a+(b+c) = (a+b)+c;

Note that the second rule regarding distributivity of multiplication should be trivial to realize knowing commutation of multiplication. However, it seems to require an explicit declaration of its own lest it yield a less than completely simplified result.

For instance, take the problem of simplifying the following expression


Let us take the bare minimum number of rules to simplify the following expression namely

ab = ba; (a+b)c = ac+bc; a(bc) = (ab)*c; a+(b+c) = (a+b)+c;

The interpreter will raise the following warnings

warning: rule never reduced: (a+b)c = ac+bc; warning: rule never reduced: a(bc) = ab*c;

Essentially, what it is saying is the first rule (ab = ba;) is infinitely recursive. Alternatively, there is no set number of iterations regarding when to stop evaluating the rule, which can be true. However, allowing capping the number of iterations can be problematic as well as will be discussed later. To fix this problem one might add a commutation rule namely

(ab) - (ba) = 0;

However, there has been nothing said about subtraction in the rules and it would be unreasonable for the interpreter in all abstraction to figure out this rule without unnecessary overhead. Alternatively, many more rules could be added to allow subtraction, but we will ignore this for now and instead focus on the anti-commutator rule, which uses addition, which has been fairly well explained. Thus, the rule will read

(ab) + (ba) = 2ab;

Though, by doing this we have ignore the fact that it is now difficult to discern that the two rules of distributivity are the same without adding undesirable expectations on the interpreter. So, the two forms must now be stated explicitly as shown.

(a+b)c = ac+bc; a(b+c) = ab+ac;

Furthermore, it is worthing noting that as soon as an expression does contain subtraction, both the commutator and anti-commutator rule may be needed. Combining all these rules together, we know have the following

(ab)+(ba) = 2ab; (a+b)c = ac+bc; a(b+c) = ab+ac; a(bc) = (ab)c; a+(b+c) = (a+b)+c;

Now, these can be applied on our previous expression


to obtain the following


Well, this is somewhat unsatisfying especially as we can see the expression that should be reduced (by the anti-commutator) in the result (note removing the parenthesis in the anti-commutator rule has no effect). The problem can be resolve by adding associative expression for addition namely

(a+b)+c+d = a+(b+c)+d; a+(b+c)+d = (a+b)+c+d;

which gives us the desired result


However, this fails as soon as it is applied to


Note that without the previous addition rules, the expression can be simplified without using the commutator rule. Not to mention that creating multiple associativity rules like this creates an enormous amount of redundancy in any code leading to an increased chance of a variety of bugs occurring.

Though one can easily simplify the given expression without the help of the rules in this case, adding many more terms makes it more complex. How would one simplify the following expression


which yields this


Though, the computer was able to generate and keep track of this sequence of terms from a few simple rules. It would be difficult for an individual to do so or for that matter use this output. Furthermore, telling the computer to evaluate an expression like this with particular numbers would quickly become expensive.

The main advantage of using rules to engage in expression rewriting (in terms of evaluating mathematical expressions) is to preform a generally low cost operation before preforming a high cost operation (calculating). However, to do this effectively, a number of things must happen. First, it is useful to group like terms, which requires knowing what terms have similar composition (both ab and ba has the same variables a and b). Secondly, it requires the knowledge of how to commute (or permute) terms (both * and + are invariant under commutation (or permutation) of their arguments).

Recognizing like compositions is not difficult given a unique ordering for a unique set of terms (sorted variable names or something similar). However, as has been demonstrated through this example, commutation is somewhat difficult to formulate under the current rules. Determining a method of describing commutation without loss of generality while still making it largely applicable is also difficult. Finding a method of describing permutations of arguments in a simple and explicit way has massive benefits in terms of later computation, readability of results, and simplicity of code. If there is already a mechanism to do this and I have missed it, please let me know. If not, I would be happy to help others solve this problem.

Comments (2)

  1. Albert Graef

    (Sorry for the very late reply, seems I missed your issue when you first posted it.)

    If I understand you correctly, you're asking for rewriting modulo AC (associativity-commutativity). This is really beyond Pure's scope right now. There are other rewriting engines which do this (mostly related to equational theorem provers). In Pure you can work around this limitation with local rule sets and making good use of term orders or similar explicit normalization strategies which will give you the normal forms that you want. But it's really better to take this discussion to the mailing list if you're still interested.

  2. Log in to comment