Small comment. Marcin wrote:

About program transformation possibility: I don't see how it would be applied in practice. There is no use of associativity of (+) for the compiler. It can do many optimizations, but it won't rewrite x+(y+z) to (x+y)+z nor vice versa.

Associativity and commutativity (AC) are not optimizations in themselves, but rather enable optimizations if you have an AC matcher in your rewriting system (as, for instance, in Mathematica). - Conal