I didn’t mean to suggest that all conceivable or useful notions of reduction are “bidirectional” and hence Church-Rosser. I meant that the sort of transformations relvant to the OP, the sort of rules that allow one to rewrite (1 + 2)^2 as 1^2 + 2*2 + 2^2, have this property.
If you actually look at the OP itself, it didn’t specify anything about the context. That arose later.
I suppose the title didn’t “just about say it all”.
Fair enough, but I think it’s clear by now, if not from the original post (which, by the way, talked about “simplification”, not “reduction”), that the question was about transformations of expressions according to identities. These are all Church-Rosser, no?
Well, if you mean “simplification”, then in what sense can x[sup]2[/sup] + 2x + 1 be said to simplify to (x+1)[sup]2[/sup]?
Better yet, how can x[sup]2[/sup] + 2x be said to simplify to (x+1)[sup]2[/sup] - 1?
If you’re looking for some collection of rules to convert between algebraically equivalent terms, I’m not sure the problem is quite so clear-cut. Yes, it’s easy to see that adding and subtracting a given quantity gives an equivalent expression, but to know what to add or subtract at a given step is very subtle.
The big benefit of a C-R notion of reduction is that at any point you can make any choice you want and you’ll always get “closer” to a “normal form”, which is unique. Arithmetic doesn’t really seem to have much in the way of that.