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: o1 ={x ^ a, y ^ b} and o2 = {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(Г) = {o1,o2}. ?


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: o1 = {x ^ a, y ^ b} and o2 = {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) =C f (b, a) and f (f (a, b), f (a, b)) =I f (a, b) we have two unifiers: o1 = {x ^ a, y ^ b} and o2 = {x ^ b, y ^ f (a, b)}. Both unifiers are ground and not encompassment equivalent, hence the result. ?

< Prev   CONTENTS   Source   Next >