# Commutativity

The equational theory C consisting of the single axiom *C = {f (x, y) = f (y, x*)} is also one of the first axioms that has been investigated alone and in combination with other axioms. It is well-known that this theory is finitary [74] and since the set of essential unifiers is a subset of the set of most general unifiers, we have:

Theorem 11.8 *The set of essential unifiers for commutativity is e-finitary*

Unfortunately however it does not collapse into an e-unitary theory within our current definitional framework:

Theorem 11.9 *The theory of commutativity is not e-unitary*

*Proof* Consider the problem *Г = {f (x, y) =***C ***f (a, b)}* which has two unifiers: *o _{1} ={x* ^

*a, y*^ b} and

*o*^

_{2}= {x*b, y*^ a}. Both unifiers are ground with a single constant symbol, so obviously they do not encompass any other unifier. Hence

*eU*?

_{C}*(Г) = {o*}. ?

_{1},o_{2}# Idempotency

The theory *I = {f (x, x) = x}* is also well-known as a finitary theory and similar to C it is also not e-unitary:

Theorem 11.10 *The theory of idempotency is not e-unitary*

Consider the problem *Г = {f* (*f (a, x), f (y, b))* =? *f (a, b)}* which has two unifiers: o_{1} *= {x* ^ *a, y* ^ *b}* and o_{2} *= {x* ^ *b, y* ^ *a}* and since both unifiers are ground and they do not encompass any other unifier, they are both in *eU ? _{I} (Г), *hence the theory is e-finitary.

Finally we have

Theorem 11.11 *The theory of idempotency and commutativity is e-finitary*

*Proof* It is known that IC is finitary [66], but could it be e-unitary? Unfortunately not, because consider the problem *Г = {f* (*f (a, x), y) =? _{CI} f (a, b)}.* Since

*f (a, b) =*and

_{C}f (b, a)*f*(

*f (a, b), f (a, b)) =*we have two unifiers: o

_{I}f (a, b)_{1}=

*{x ^ a, y ^ b}*and o

_{2}

*= {x ^ b, y ^ f (a,*b)}. Both unifiers are ground and not encompassment equivalent, hence the result. ?