# Essential E-Unification

In Sect.2.4 we showed the steps for the extension of the subsumption quasiorder for terms to substitutions and then extended it to equational theories *= _{E}* in order to get the concept of a most general

*E*-unifier.

However for all practical purposes, we do not only have the unpleasant situation that there are nullary *E*-unification theories [2, 30, 69], but even more importantly there is such an enormous plenitude of most general unifiers that it defies its original purpose: there are very simple theories such as associativity that are infinite and even the finite theories may have sets of most general unifiers that are beyond practical usefulness. For example the theory of associativity and commutativity AC has exponentially many unifiers, in fact for a base *B* there are *B* with a tower of exponentials manyunifiers [12, 25, 46, 47]. So the question is: can we find a more general concept for the generating set, than the set of most general unifiers. As a step in this direction we propose the notion of an essential unifier, whose definition is not based on the generality order of the past, but on the encompassment order lifted to substitutions and extended to equational theories. So the concept of an essential *E*-unifier is as follows:

Definition 11.5 *(essential E-unifier)*

- 1. An
*E*-unifier*a*for a unification problem*Г*modulo the equational theory E and the variables*V**=*Var*(Г),*is*encompassed*by an*E*-unifier*т*for*Г*, denoted as above by*a**c.*^{V}E*т*, if there exists a substitution X, such that*(aX)*|_{V}is a subsubstitution of*т*. - 2. An
*E*-unifier*a*for a unification problem*Г*modulo the equational theory*E*that does not encompass any other*E*-unifier for*Г*is called an*essential E*-*unifier*. We denote the set of essential*E*-unifiers as*eU*?_{E}*(Г).*Two unifiers*a*and*т*are*encompassment equivalent modulo E,*denoted*«*, if^{V}E*a*^E т and*т**c**.*^{V}E*a*. - 3. A
*complete*set of*essential E*-unifiers for*Г*is a set of*E*-unifiers, such that for each*E*-unifier*т*there exists*a*in the set with*a**c**.'**E**т*. - 4. The set
*eU ?*_{E}*(Г)*is called a*minimal complete set*of*essential E*-unifiers for*Г*, or simply*the set of essential E-unifiers for Г*, if it is a complete set and for all*a*and*a**'*in*eU ?*_{E}*(Г) a*and*a**'*are encompassment equivalent.

Proposition 11.1 *The encompassment order on substitutions is a quasiorder, that is, it is reflexive and transitive.*

*Proof* reflexivity: *a* c_{E} *a* means that there are substitutions X_{b} *X*_{2}* **: **a **= _{E} *

*X*

_{1}*aX*

_{2}*,*setting Xi and X

_{2}to the substitution identity

*e*we have

*a*

*=*

_{E}*eae*

*=*

*a*.

transitivity: *a **c. ^{V}E *

*т*and

*т*

*c.*

^{V}E*f*implies

*a*

*c.*

^{V}E*f*, where by definition we have Dom(a) = Dom^) = Dom(f) =:

*V*, so

which implies

?

A well known property of unification in the free term algebra is that the most general unifier is unique (up to renaming of variables), if the unification problem is solvable. This is a property we would like to have for sets of essential unifiers as well.

One way to generate the set of all E-unifiers from the minimal set of most general unifiers, *p** U* ?

*is via a closure operator. The notion of a*

_{E}(Г),*closure operator*is well established and plays a central role in many areas of algebra, computational logic and mathematics in general (see for example [29]). For a set

*M*a mapping

**C***:*

*(*

**P***M*) ^

*(*

**P***M*) from the power set of

*M*to itself, is a

*closure operator*if it is extensive, monotone increasing and idempotent. It can be shown that the set

*e*

*?*

**U**_{e}

*(Г)*of essential unifiers can be closed and generates all E-unifiers for

*Г*as well.

Proposition 11.2 *The set of essential unifiers e***U ***? _{E} (Г) is unique up to part equivalence *k

_{e}.*Proof* Suppose it is not unique, then there would be two complete sets of essential unifiers *e** U* ?E and

*e*

**U***?*

^{2}*. Let o*

_{E}_{2}be in

*e*

**U***?*

^{2}

_{E}e*?E, now because*

**U***e*

*?E is complete, there exists some r*

**U**_{1}in

*e*

*?E which encompasses*

**U***o*

*: t*

_{2}*c*

_{1}_{e}o

_{2}. On the other hand, because

*e*

**U***?*

^{2}*is a set of essentials, i.e. in particular it is also complete, there exists*

_{E}*o*

*in*

_{3}*e*

**U***?*

^{2}*with*

_{E}*o*

*c*

_{3}_{E}r

_{1}. But then

*o*

*c*

_{3}_{E}t

*c*

_{1}_{e}o

_{2}and by transitivity we have o

_{3}c

_{E}o

_{2}, contradicting the assumption that

*e*

**U***?*

^{2}*is minimal. ?*

_{E}Lemma 11.1 *The set of essential unifiers of a non nullary unification problem Г is a subset of the set of most general unifiers: e***U ***? _{E} (Г)* с

*д*

**U***?*

_{E}(Г).*Proof* This follows easily from the fact that the subsumption order is a special case of encompassment, where Л_{1} is the empty substitution e. More explicitly: if *o* is an essential *E* -unifier, it is not encompassed by any other unifier, hence it is not subsumed by any other unifier either. ?

The important observation is that the set of essential *E* -unifiers can be *lovely,* that is, it can be extremely small in comparison to its superset of most general unifiers. The results currently known in this small subfield of unification theory—that is still at its infancy and under development—are summarized in Sect. 11.4.