Lambda the Ultimate

Commutativity of operations and functions can be a useful thing for a compiler to know. So how do you you tell the compiler an operator or function is commutative (or associative, etc.)? One obvious option would be to let programmers tag their functions. This is bound to introduce subtle and nasty errors in to the code if the programmer makes a mistake. Not to mention it is inelegant, and it isn’t the kind of thing I want to see mixed in people's code (optimization hints that is).

So the big question is, how do we automatically recognize proprerties of functions like commutativity? In Cat (like Haskell) there is already a system for expressing rewriting rules (e.g. rule { $a $b f } => { $b $a f }). This fairly obviously demonstrates the commutativity of 'f'. In fact if we can follow any sequence of rewriting rules to arrive at this equality (which is a simple graph search problem), then we can also deduce commutativity.

I am trying to track down related research on the subject. If anyone has any pointers, I would be most appreciative.