# rule transformations for compositions of tensor products

The tensor product satisfies far commutativity:

$(f \circ g) \otimes (h \circ k) =(f \otimes h) \circ (g \otimes k)$.

I have some replacement rules I'd like to apply to an expression containing tensor products and compositions. For example, whenever $(a \otimes b) \circ (c \otimes d)$ appears, I might like to replace it with $l$. The problem is that applying far commutativity in an a prespecified way (for example, lhs -> rhs) cannot guarantee that $(a \otimes b) \circ (c \otimes d)$ appears as a subexpression of the result, even if it is implicitly present.

I therefore need to search the space of far-commutativity-transformed expressions and apply certain replacement rules when I can. I know that the space of expressions far-commutativity-equivalent to a given one is finite, after all possible replacements are performed the process terminates, and the result does not depend on the order of the replacements.

This seems like the sort of term-rewriting problem for which Mathematica might have an automatic capability. Is there a short, readable, and relatively efficient way to do it?

-
Can you maybe give an example of an expression that does not succumb to your attempts at term-rewriting? –  Ｊ. Ｍ. Apr 17 '13 at 7:42
I'm worried that I'll get solutions for a series of examples I suggest and then get accused of moving the goalposts after a certain number of such examples. But for instance, say you have an n-fold composition of n-fold tensor products of functions (represented by undefined symbols). To make far-commutativity easy to deal with for this case, assume all functions have the same domain and range. Find all instances of $(a\otimes c)\circ (b\otimes d)$, to be replaced with e. For example, in $(a\otimes c\otimes f)\circ (b\otimes d\otimes g)\circ (h\otimes k\otimes l)$, it appears as a... –  Tobias Hagge Apr 17 '13 at 8:25
...subexpression after appropriate far commutativity changes. –  Tobias Hagge Apr 17 '13 at 8:26
I see that my expression in the second paragraph is the same as that in the first, this was accidental, and confusing. I'll edit. –  Tobias Hagge Apr 17 '13 at 8:27
So, in that example, the output should be $(e \otimes (f \circ g)) \circ (h \otimes k \otimes l)$, or something far-commutativity-equivalent to that. –  Tobias Hagge Apr 17 '13 at 8:33