A binary operation $f$ that is associative and satisfies $f(f(x,y),x)\approx x$

Question

"Let $f$ a binary function symbol, and $$E=\{f(x,f(y,z)) \approx f(f(x,y),z), f(f(x,y),x) \approx x\}$$ a set of identities. Show that $f(x,x) (\leftrightarrow_E)^* x$ and $f(f(x,y),z) (\leftrightarrow_E)^* f(x,z)$." I am using the definitions in the Baader Book of Rewriting Systems, where this $(\leftrightarrow_E)^*$ relationship is closed under substitutions and compatible with $\sum$-operations. I managed to do the first part, doing some manipulations, but I'm not able to do the second part.

Answer 1

First, some psychological simplification. I'll use juxtaposition notation in place of $f$, so "$f(t_1,t_2)$" will be written "$t_1t_2$." This makes it a bit easier to write out the relevant steps. Moreover, given the associativity of $f$ (your first axiom), we can include or omit parentheses as we please.

With this in mind, you want to get from "$xyz$" to "$xz$" using associativity and the equation $uvu=u$. Well, by omitting parentheses we've essentially "maximally used" associativity already, so the only thing left to do is find some clever way to apply that remaining equation. There are no terms of the form $uvu$ involved, so we have to pick some existing term $u$ and replace it with $uvu$ for some term $v$ of our choice.

A big part of our goal is to get rid of $y$, and the only way we can get rid of a symbol is by using the $uvu\leadsto u$-direction of the axiom. Since $y$ is flanked on the right by $z$, this tells us that we'd be really happy if we could get a $z$ to show up somewhere to the left of $y$. The only thing to the left of $y$ right now is $x$, so this suggests the following choice of $u$ and $v$ for applying the "lengthening" rule $u\leadsto uvu$:

Set $u=x$ and $v=z$. This will give as our new string $$xzxyz.$$

Now this has a substring of the form $z[stuff]z$, so we can - by applying the "shortening" rule $uvu\leadsto u$, with $u=z$ and $v=[stuff]$ - collapse that to just $z$. And at that point:

We're done: throwing in parentheses for clarity, we have $$xzxyz=x(z(xy)z)=xz.$$

Hopefully the explanation above makes this seem not ad hoc; I think the "goal-directed" language I used is often helpful, but that's just my experience. (Of course I haven't actually written the above in the literal form of an $\leftrightarrow_E^*$-derivation, but the translation into that format is straightforward.)