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.VE т, 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 «VE, if a ^E т and т c.VE 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 cE a means that there are substitutions Xb X2 : a =E X1aX2, setting Xi and X2 to the substitution identity e we have a =E eae = a.
transitivity: a c.VE т and т c.VE f implies a c.VE f, where by definition we have Dom(a) = Dom^) = Dom(f) =: V, so
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, pU ?E(Г), is via a closure operator. The notion of a closure operator is well established and plays a central role in many areas of algebra, computational logic and mathematics in general (see for example ). 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 eU ?e(Г) of essential unifiers can be closed and generates all E-unifiers for Г as well.
Proposition 11.2 The set of essential unifiers eU ?E (Г) is unique up to part equivalence ke.
Proof Suppose it is not unique, then there would be two complete sets of essential unifiers eU ?E and eU ?2E. Let o2 be in eU ?2EeU ?E, now because eU ?E is complete, there exists some r1 in eU?E which encompasses o2: t1 ce o2. On the other hand, because eU ?2E is a set of essentials, i.e. in particular it is also complete, there exists o3 in eU ?2E with o3 cE r1. But then o3 cE t1 ce o2 and by transitivity we have o3 cE o2, contradicting the assumption that eU?2E is minimal. ?
Lemma 11.1 The set of essential unifiers of a non nullary unification problem Г is a subset of the set of most general unifiers: eU ?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.