The Unification Type of an Equational Theory May Depend on the Instantiation Preorder

Suppose there exists a chain ${\sigma }_1{>}_E^X{\sigma }_2{>}_E^X{\sigma }_3{>}_E^X\mathrm{\cdots }$ satisfying the conditions stated in the lemma. This chain satisfies the following properties:

1. 1.

   It has no lower bound in ${𝒰}_E(\mathrm{\Gamma })$, i.e., there is no $E$-unifier $\tau$ of $\mathrm{\Gamma }$ such that ${\sigma }_i{\ge }_E^X\tau$ for all $i\ge 1$. To see why this is true, suppose such a unifier $\tau$ does exist. Since $𝒮$ is complete, there is $j\ge 1$ such that $\tau {\ge }_E^X{\sigma }_j{>}_E^X{\sigma }_{j+1}{\ge }_E^X\tau$. Transitivity of ${\ge }_E^X$ yields that ${\sigma }_{j+1}{\ge }_E^X{\sigma }_j$, but this contradicts ${\sigma }_j{>}_E^X{\sigma }_{j+1}$.

2. 2.

   For all $i\ge 1$, if there is $\tau \in {𝒰}_E(\mathrm{\Gamma })$ such that ${\sigma }_i{\ge }_E^X\tau$, then there exists ${\tau }^{\prime }\in {𝒰}_E(\mathrm{\Gamma })$ such that $\tau {\ge }_E^X{\tau }^{\prime }$ and ${\sigma }_{i+1}{\ge }_E^X{\tau }^{\prime }$. To show this, assume that ${\sigma }_i{\ge }_E^X\tau$. The completeness of $𝒮$ yields $j\ge 1$ such that ${\sigma }_i{\ge }_E^X\tau {\ge }_E^X{\sigma }_j$. This implies that ${\sigma }_i{\ge }_E^X{\sigma }_j$ because ${\ge }_E^X$ is a transitive relation. Hence, since the chain is strictly decreasing, it follows that $i\le j$, and thus ${\sigma }_{i+1}{\ge }_E^X{\sigma }_{j+1}$ and $\tau {\ge }_E^X{\sigma }_{j+1}$. Consequently, we can set ${\tau }^{\prime }:={\sigma }_{j+1}$.

Now, let $M$ be the set of ${⪯}_E^X$-minimal elements of ${[{𝒰}_E(\mathrm{\Gamma })]}_E^X$. To prove that $\mathrm{\Gamma }$ has type zero, it suffices to show that $M$ is not complete. Assume to the contrary that $M$ is complete. Then there exists ${[\tau ]}_E^X\in M$ such that ${[\tau ]}_E^X{⪯}_E^X{[{\sigma }_1]}_E^X$, and thus ${\sigma }_1{\ge }_E^X\tau$. Since our chain does not have a lower bound, there must be an $i\ge 1$ such that ${\sigma }_i{\ge }_E^X\tau$ and ${\sigma }_{i+1}{\ngeqq }_E^X\tau$. Using the second property shown for our chain, there exists a unifier ${\tau }^{\prime }$ such that $\tau {\ge }_E^X{\tau }^{\prime }$ and ${\sigma }_{i+1}{\ge }_E^X{\tau }^{\prime }$. Minimality of ${[\tau ]}_E^X$ implies that $\tau {\sim }_E^X{\tau }^{\prime }$, and thus ${\sigma }_{i+1}{\ge }_E^X{\tau }^{\prime }{\ge }_E^X\tau$, which yields a contradiction. Thus, we have shown that $M$ cannot be complete, which implies that $\mathrm{\Gamma }$ has type zero. $◀$

As usual, we order unification types w.r.t. how bad they are (larger is worse) by setting

zero $>$ infinitary $>$ finitary $>$ unitary.

The unification type w.r.t. ${\le }_E^X$ of an equational theory $E$ is the worst type of any solvable $E$-unification problem w.r.t. ${\le }_E^X$. The unrestricted unification type of $\mathrm{\Gamma }$ ($E$) is the one w.r.t. ${\le }_E^V$ and the restricted unification type of $\mathrm{\Gamma }$ ($E$) is the one w.r.t. ${\le }_E^X$ for $X=\mathrm{Var}(\mathrm{\Gamma })$.

The results on the unification type of equational theories in the literature are usually shown for the restricted case. As we will demonstrate in this paper, it may indeed make a considerable difference for the unification type which instantiation preorder is employed in its definition. This is however not the case in the following situation.

Let $𝒮$ be a minimal complete set of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^X$. For every unifier $\theta$ in $𝒮$ we can rename the variables in $\mathrm{VRan}(\theta )$ such that they do not belong to $X$ by applying an appropriate permutation $\pi$ that maps the variables of $\mathrm{VRan}(\theta )$ bijectively to a set of variables $Y$ with $|Y|=|\mathrm{VRan}(\theta )|$ and $Y\cap (X\cup \mathrm{VRan}(\theta ))=\mathrm{\varnothing }$. Such a finite set $Y$ of variables exists since $\mathrm{VRan}(\theta )$ is finite and $V\setminus X$ is infinite. For a given bijection $p:\mathrm{VRan}(\theta )\to Y$, we can define $\pi$ as follows: $\pi (z):=p(z)$ for all $z\in \mathrm{VRan}(\theta )$, $\pi (y):=p^{-1}(y)$ for all $y\in Y$, and $\pi (x)=x$ for all other variables. Note that $\pi$ is a substitution since its domain is $\mathrm{VRan}(\theta )\cup Y$, which is finite. To show that $\pi$ really is a permutation, i.e., a bijective mapping from $V$ to $V$, it is sufficient to show that it is an injective mapping from $V$ to $V$ (see Lemma 2.6 in [28]). This is an immediate consequence of the facts that $p$ and $p^{-1}$ are bijections and $Y$ and $\mathrm{VRan}(\theta )$ are disjoint.

The substitution $\pi \theta$ is equivalent to $\theta$ w.r.t. the equivalence relation ${\sim }_{\mathrm{\varnothing }}^V$ induced by ${\le }_{\mathrm{\varnothing }}^V$, and thus also w.r.t. ${\sim }_E^X$. In fact, ${\pi }^{-1}\pi \theta =\theta$. If we restrict the domain of this substitution to $X$, then the resulting substitution ${\pi \theta |}_X$ is still equivalent to $\theta$ w.r.t. ${\sim }_E^X$ and also satisfies $\mathrm{VRan}({\pi \theta |}_X)\cap X=\mathrm{\varnothing }$. To see the latter, consider a variable $x\in \mathrm{Dom}({\pi \theta |}_X)$. First assume that $x\in \mathrm{Dom}(\theta )\cap X$. Then all the variables in $\theta (x)$ belong to $\mathrm{VRan}(\theta )$, and thus all the variables in ${\pi \theta |}_X(x)$ belong to $Y$, which is disjoint with $X$. If $x\in X\setminus \mathrm{Dom}(\theta )$, then ${\pi \theta |}_X(x)=\pi (x)\ne x$. Since $\mathrm{Dom}(\pi )=\mathrm{VRan}(\theta )\cup Y$ and $Y$ is disjoint with $X$, this implies $x\in \mathrm{VRan}(\theta )$, and thus $\pi (x)\in Y$.

Let ${𝒮}^{\prime }$ be the set of substitutions obtained from $𝒮$ by applying this renaming and domain restriction process to every element of $𝒮$. Due to the ${\sim }_E^X$-equivalence of the elements of $𝒮$ with their modified variants in ${𝒮}^{\prime }$ and the fact that $X$ contains all the variables occurring in $\mathrm{\Gamma }$, it is easy to see that ${𝒮}^{\prime }$ is also a minimal complete set of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^X$. In a second step, we restrict the domains of the elements of ${𝒮}^{\prime }$ to $X_0$. Given an element $\theta$ of ${𝒮}^{\prime }$, we define ${\theta |}_{X_0}$ to be the substitution that coincides with $\theta$ on $X_0$ and maps each variable $x\notin X_0$ to $x$. Since $\theta$ is an $E$-unifier of $\mathrm{\Gamma }$ and this unification problem contains only variables from $X_0$, the substitution ${\theta |}_{X_0}$ is clearly also an $E$-unifier of $\mathrm{\Gamma }$. We claim that ${\theta |}_{X_0}{\le }_E^X\theta$. To prove this, we define the substitution $\lambda$ by setting $\lambda (x):=\theta (x)$ if $x\in X\setminus X_0$ and $\lambda (x):=x$ for all other variables. We now show that ${\lambda \theta |}_{X_0}{\approx }_E^X\theta$. If $x\in X_0\cap \mathrm{Dom}(\theta )$, then $\lambda ({\theta |}_{X_0}(x))=\lambda (\theta (x))=\theta (x)$. The first identity holds by the definition of ${\theta |}_{X_0}$ and the second since the variables occurring in $\theta (x)$ are elements of $\mathrm{VRan}(\theta )$, and thus do not belong to $X$. If $x\in X_0\setminus \mathrm{Dom}(\theta )$, then $\lambda ({\theta |}_{X_0}(x))=\lambda (x)=x=\theta (x)$. Finally, if $x\in X\setminus X_0$, then $\lambda ({\theta |}_{X_0}(x))=\lambda (x)=\theta (x)$. Again, the first identity holds by the definition of ${\theta |}_{X_0}$ and the second by the definition of $\lambda$. Summing up, we have shown that the following holds for every element $\theta$ of ${𝒮}^{\prime }$: ${\theta |}_{X_0}$ is an $E$-unifier of $\mathrm{\Gamma }$ and ${\theta |}_{X_0}{\le }_E^X\theta$. Since ${𝒮}^{\prime }$ is a minimal complete set of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^X$, its elements are minimal w.r.t. ${\le }_E^X$, which yields ${\theta |}_{X_0}{\sim }_E^X\theta$. Consequently, we know that the set ${{𝒮}^{\prime }|}_{X_0}:=\{{\theta |}_{X_0}\mid \theta \in {𝒮}^{\prime }\}$ is also a minimal complete set of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^X$.

We claim that the same is true w.r.t. the smaller set of variables $X_0$, i.e., that ${{𝒮}^{\prime }|}_{X_0}$ is also minimal and complete w.r.t. ${\le }_E^{X_0}$. Completeness trivially follows from the fact that ${\le }_E^X\subseteq {\le }_E^{X_0}$. To prove minimality, assume that $\theta$ and $\tau$ are two distinct elements of ${{𝒮}^{\prime }|}_{X_0}$. Then these two substitutions are not comparable w.r.t. ${\le }_E^X$. Assume that they are comparable w.r.t. ${\le }_E^{X_0}$, i.e., there is a substitution $\lambda$ such that $\lambda (\theta (x)){\approx }_E\tau (x)$ holds for all $x\in X_0$. By our construction of ${{𝒮}^{\prime }|}_{X_0}$, we know that $\mathrm{Dom}(\theta )\subseteq X_0$, $\mathrm{Dom}(\tau )\subseteq X_0$, and $\mathrm{VRan}(\theta )\cap X=\mathrm{\varnothing }$. If $x$ is a variable in $X\setminus X_0$, then $\lambda (\theta (x))=\lambda (x)$ and $\tau (x)=x$. Thus, if we modify $\lambda$ to ${\lambda }^{\prime }$ such that ${\lambda }^{\prime }(x)=x$ holds for all $x\in X\setminus X_0$, then ${\lambda }^{\prime }(\theta (x))=\tau (x)$ holds for all $x\in X\setminus X_0$. This modification has no effect on the variables $x\in X_0$. In fact, let $x$ be such a variable. If $x\in \mathrm{Dom}(\theta )$, then $\theta (x)$ does not contain any variable from $X$, and thus ${\lambda }^{\prime }(\theta (x))=\lambda (\theta (x)){\approx }_E\tau (x)$ holds. If $x\notin \mathrm{Dom}(\theta )$, then $\theta (x)=x$, and thus again ${\lambda }^{\prime }(\theta (x))={\lambda }^{\prime }(x)=\lambda (x)=\lambda (\theta (x)){\approx }_E\tau (x)$ since ${\lambda }^{\prime }$ coincides with $\lambda$ on the variables in $X_0$. Summing up, we have shown that the assumption $\theta {\le }_E^{X_0}\tau$ implies $\theta {\le }_E^X\tau$, which contradicts the fact that ${{𝒮}^{\prime }|}_{X_0}$ is minimal w.r.t. ${\le }_E^X$. Consequently, ${{𝒮}^{\prime }|}_{X_0}$ is a minimal complete set w.r.t. ${\le }_E^{X_0}$, and this set has the same cardinality as the minimal complete set $𝒮$ of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^X$ we have started with.

Conversely, let $𝒮$ be a minimal complete set of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^{X_0}$. By applying the same construction as in the proof of the other direction, we can assume without loss of generality that every unifier $\theta \in 𝒮$ satisfies $\mathrm{Dom}(\theta )\subseteq X_0$ and $\mathrm{VRan}(\theta )\cap X=\mathrm{\varnothing }$. In fact, by applying this construction to a minimal complete set ${𝒮}^{\prime }$ of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^{X_0}$, we obtain a new set $𝒮$ where every element ${\theta }^{\prime }$ of the original set ${𝒮}^{\prime }$ is replaced with an element $\theta$ that satisfies the above conditions and is ${\sim }_E^X$-equivalent to ${\theta }^{\prime }$, and thus also ${\sim }_E^{X_0}$-equivalent. Consequently, this new set $𝒮$ is also a minimal complete set of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^{X_0}$.

We claim that $𝒮$ is also minimal and complete w.r.t. the larger set of variables $X$. Minimality trivially follows from the fact that ${\le }_E^X\subseteq {\le }_E^{X_0}$. To prove completeness, assumed that $\tau$ is an $E$-unifier of $\mathrm{\Gamma }$. Completeness of $𝒮$ w.r.t. ${\le }_E^{X_0}$ yields an element $\theta$ of $𝒮$ such that $\theta {\le }_E^{X_0}\tau$, i.e., there is a substitution $\lambda$ such that $\lambda \theta (x){\approx }_E\tau (x)$ holds for all $x\in X_0$. Let $x$ be a variable in $X\setminus X_0$. Then $\lambda \theta (x)=\lambda (x)$. Thus, if we modify $\lambda$ to ${\lambda }^{\prime }$ such that ${\lambda }^{\prime }(x)=\tau (x)$ holds for all $x\in X\setminus X_0$, then ${\lambda }^{\prime }(\theta (x))=\tau (x)$ holds for all $x\in X\setminus X_0$. The claim that this modification has no effect for the variables $x\in X_0$ can be shown as in the proof of minimality of ${{𝒮}^{\prime }|}_{X_0}$ w.r.t. ${\le }_E^{X_0}$ above. This proves that ${\lambda }^{\prime }\theta (x){\approx }_E\tau (x)$ holds for all $x\in X$, and thus $𝒮$ is also complete w.r.t. ${\le }_E^X$. $◀$

The following theorem is an immediate consequence of this lemma.

Note that the condition of the theorem is in particular satisfied if $X$ is a finite superset of $\mathrm{Var}(\mathrm{\Gamma })$. However, it is clearly not satisfied for $X=V$, which corresponds to the unrestricted instantiation preorder setting. We will see below that in this case the unification type can indeed depend on whether the restricted or the unrestricted instantiation preorder is used. However, there is a special case where this cannot happen.

Let $𝒮$ be a minimal complete set of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^V$. Since ${\le }_E^V\subseteq {\le }_E^{\mathrm{Var}(\mathrm{\Gamma })}$, this set is also complete w.r.t. ${\le }_E^{\mathrm{Var}(\mathrm{\Gamma })}$. To show minimality w.r.t. ${\le }_E^{\mathrm{Var}(\mathrm{\Gamma })}$, assume to the contrary that $\sigma ,\theta$ are two distinct elements of $𝒮$ such that $\sigma {\le }_E^{\mathrm{Var}(\mathrm{\Gamma })}\theta$, i.e., there is a substitution $\lambda$ such that $\lambda \sigma (x){\approx }_E\theta (x)$ holds for all $x\in \mathrm{Var}(\mathrm{\Gamma })$. We modify $\lambda$ to ${\lambda }^{\prime }$ by setting ${\lambda }^{\prime }(x)=x$ for all variables $x\in V\setminus \mathrm{Var}(\mathrm{\Gamma })$. For $x\in \mathrm{Var}(\mathrm{\Gamma })$, we know that $\sigma (x)$ contains only variables from $\mathrm{VRan}(\sigma )\subseteq \mathrm{Var}(\mathrm{\Gamma })$ if $x\in \mathrm{Dom}(\sigma )$ or $\sigma (x)=x\in \mathrm{Var}(\mathrm{\Gamma })$. Since $\lambda$ and ${\lambda }^{\prime }$ coincide on $\mathrm{Var}(\mathrm{\Gamma })$, this yields ${\lambda }^{\prime }\sigma (x)=\lambda \sigma (x){\approx }_E\theta (x)$. For $x\in V\setminus \mathrm{Var}(\mathrm{\Gamma })$, this variable does not belong to any of the sets $\mathrm{Dom}(\sigma )$, $\mathrm{Dom}(\theta )$, and $\mathrm{Dom}({\lambda }^{\prime })$, and thus ${\lambda }^{\prime }\sigma (x)={\lambda }^{\prime }(x)=x=\theta (x)$. Summing up, we have shown that $\sigma {\le }_E^V\theta$, which contradicts our assumption that $𝒮$ is minimal w.r.t. ${\le }_E^V$.

Conversely, assume that $𝒮$ is a minimal complete set of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^{\mathrm{Var}(\mathrm{\Gamma })}$. Since ${\le }_E^V\subseteq {\le }_E^{\mathrm{Var}(\mathrm{\Gamma })}$, minimality also holds w.r.t. ${\le }_E^V$. To show completeness w.r.t. ${\le }_E^V$, assume that $\theta$ is an $E$-unifier of $\mathrm{\Gamma }$. Completeness of $𝒮$ w.r.t. ${\le }_E^{\mathrm{Var}(\mathrm{\Gamma })}$ yields a substitution $\sigma \in 𝒮$ such that $\sigma {\le }_E^{\mathrm{Var}(\mathrm{\Gamma })}\theta$. Similarly to the first part of the proof, we can show that this also implies $\sigma {\le }_E^V\theta$. The difference is that now $\theta$ is an arbitrary unifier, and thus $\mathrm{VRan}(\theta )\cup \mathrm{Dom}(\theta )\subseteq \mathrm{Var}(\mathrm{\Gamma })$ need not hold. Let $\lambda$ be such that $\lambda \sigma (x){\approx }_E\theta (x)$ holds for all $x\in \mathrm{Var}(\mathrm{\Gamma })$. We modify $\lambda$ to ${\lambda }^{\prime }$ by setting ${\lambda }^{\prime }(x)=\theta (x)$ for all variables $x\in V\setminus \mathrm{Var}(\mathrm{\Gamma })$. For $x\in \mathrm{Var}(\mathrm{\Gamma })$, we obtain ${\lambda }^{\prime }\sigma (x)=\lambda \sigma (x){\approx }_E\theta (x)$ as in the first part of the proof. For $x\in V\setminus \mathrm{Var}(\mathrm{\Gamma })$, this variable does not belong to $\mathrm{Dom}(\sigma )$, and thus ${\lambda }^{\prime }\sigma (x)={\lambda }^{\prime }(x)=\theta (x)$. $◀$

Examples of equational theories where the conditions of this theorem are always satisfied are the empty theory (unitary), the theory $𝖢$ axiomatizing commutativity of a binary function symbol (finitary), and the theory $𝖠$ axiomatizing associativity of a binary function symbol (infinitary). This is an easy consequence of the known algorithms [42, 50, 45] computing (or enumerating, in the case of $𝖠$) minimal complete sets of unifiers for these theories.

The following result is an easy consequence of the fact that ${\le }_E^V\subseteq {\le }_E^{\mathrm{Var}(\mathrm{\Gamma })}$.

A given finite minimal complete set $𝒮$ of $E$-unifiers of $\mathrm{\Gamma }$ w.r.t. ${\le }_E^V$ is also complete w.r.t. ${\le }_E^{\mathrm{Var}(\mathrm{\Gamma })}$. If it is not minimal (which can only happen in the finitary case), then one can make it minimal by removing redundant element (i.e., elements $\theta$ such that $𝒮$ contains an element ) without destroying completeness. $◀$

Let $\sigma$ be an $ℰℒ$-unifier of $\mathrm{\Gamma }$ and $C:=\sigma (y)$ and $D:=\sigma (x)$. Then $\exists r.C⊑D$. In addition, we can assume without loss of generality that $C$ and $D$ are reduced. The characterization of subsumption in $ℰℒ$ (see Corollary 10) yields $D=\exists r.D_1\sqcap \mathrm{\dots }\sqcap \exists r.D_n$ for $n\ge 0$ $ℰℒ$ concept descriptions $D_1,\mathrm{\dots },D_n$ satisfying $C⊑D_1,\mathrm{\dots },C⊑D_n$ (see Lemma 11). Thus, if we define $\lambda :=\{z_1\mapsto D_1,\mathrm{\dots },z_n\mapsto D_n,z\mapsto C\}$, then $\lambda {\sigma }_n{\approx }_{ℰℒ}^{\{x,y\}}\sigma$, which shows ${\sigma }_n{\le }_{ℰℒ}^{\{x,y\}}\sigma$. $◀$

First note that ${\sigma }_{n+1}{\le }_{ℰℒ}^{\{x,y\}}{\sigma }_n$ since $\lambda {\sigma }_{n+1}{\approx }_{ℰℒ}^{\{x,y\}}{\sigma }_n$ for $\lambda :=\{z_{n+1}\mapsto \top \}$. Second, assume that ${\sigma }_n{\le }_{ℰℒ}^{\{x,y\}}{\sigma }_{n+1}$, i.e., there is a substitution $\tau$ such that $\tau {\sigma }_n{\approx }_{ℰℒ}^{\{x,y\}}{\sigma }_{n+1}$. Then $\exists r.\tau (z_1)\sqcap \mathrm{\dots }\sqcap \exists r.\tau (z_n){\approx }_{ℰℒ}\exists r.z_1\sqcap \mathrm{\dots }\sqcap \exists r.z_{n+1}$. Consequently, by Theorem 9, the reduced forms of these two concept descriptions would need to be equal up to associativity and commutativity of $\sqcap$. However, the reduced form of the concept description on the left-hand side has at most $n$ existential restrictions, whereas the reduced form of the concept description on the right-hand side has $n+1$ existential restrictions, which yields a contradiction. Thus, we have shown . $◀$

The following theorem is now an immediate consequence of Lemma 4.

With respect to the unrestricted instantiation preorder, the instance relationship between the substitutions ${\sigma }_n$ and ${\sigma }_{n+1}$ no longer holds. More generally, we can show the following result.

Let . Then we know from Lemma 14 that ${\sigma }_n{\nleqq }_{ℰℒ}^{\{x,y\}}{\sigma }_m$, which implies ${\sigma }_n{\nleqq }_{ℰℒ}^V{\sigma }_m$ since ${\le }_{ℰℒ}^V\subseteq {\le }_{ℰℒ}^{\{x,y\}}$.

Assume that $n>m$ and that there is a substitution $\lambda$ such that $\lambda {\sigma }_n{\approx }_{ℰℒ}{\sigma }_m$. Then $\lambda {\sigma }_n(x){\approx }_{ℰℒ}{\sigma }_m(x)$, and since ${\sigma }_m(x)$ does not contain $z_n$, but ${\sigma }_n(x)$ does, $\lambda$ must replace $z_n$ by a concept description not containing $z_n$, and thus in particular $\lambda (z_n){\not\approx }_{ℰℒ}{z}_n$. But then $\lambda {\sigma }_n(z_n)=\lambda (z_n){\not\approx }_{ℰℒ}{z}_n$ and ${\sigma }_m(z_n)=z_n$ yield a contradiction to $\lambda {\sigma }_n{\approx }_{ℰℒ}{\sigma }_m$. $◀$

Thus, w.r.t. the unrestricted instantiation preorder, the set $\{{\sigma }_n\mid n\ge 0\}$ consists of unifiers that are incomparable. However, this set is also no longer complete.

First, note that ${\sigma }_0{\le }_{ℰℒ}^V\sigma$ is not possible since ${\sigma }_0(x)=\top$, and thus $\lambda {\sigma }_0(x)=\top$ holds for all substitutions $\lambda$, whereas $\sigma (x)=\exists r.A$. If $n\ge 1$ and $\lambda {\sigma }_n{\approx }_{ℰℒ}\sigma$, then $\lambda$ must replace all variables $z_i$ occurring in ${\sigma }_n(x)$ with $A$, and thus $\lambda {\sigma }_n(z_i)=\lambda (z_i){\approx }_{ℰℒ}A$. However, $\sigma (z_i)=z_i$, which yields a contradiction to $\lambda {\sigma }_n{\approx }_{ℰℒ}\sigma$. $◀$

Summing up, we have seen that the $ℰℒ$-unification problem $\mathrm{\Gamma }$ of Example 12 has unification type zero for the restricted instantiation preorder, but the proof that we have used to show this result does not work if we employ the unrestricted instantiation preorder instead.

In the following, we prove the general result that the unrestricted unification type of $ℰℒ$ is not zero. Note that, by Theorem 8, this type cannot be unitary or finitary, and thus must be infinitary. The main idea underlying our proof of this result is to show that, up to the equivalence relation ${\sim }_{ℰℒ}^V$, every substitution has only finitely many more general substitutions w.r.t. ${\le }_{ℰℒ}^V$. The most challenging technical result needed to prove this is the following lemma.

First note that we can assume without loss of generality that $\mathrm{VRan}(\sigma )\cap \mathrm{Dom}(\theta )=\mathrm{\varnothing }$. Otherwise, we can apply a permutation to $\sigma$ that renames the variables in $\mathrm{VRan}(\sigma )$ appropriately, which yields a substitution that is ${\sim }_{ℰℒ}^V$-equivalent to $\sigma$ and satisfies the required disjointness condition (see the proof of Lemma 5 for how such a permutation can be obtained).

Since $\sigma {\le }_{ℰℒ}^V\theta$, we know that there is a substitution $\lambda$ such that $\lambda \sigma {\approx }_{ℰℒ}\theta$. Consider the set $𝒳$ of all variables $x$ such that $x\in \mathrm{Dom}(\sigma )\setminus \mathrm{Dom}(\theta )$. Then $\lambda \sigma (x){\approx }_{ℰℒ}\theta (x)=x$ holds for all $x\in 𝒳$. Consequently, the top-level conjunction of $\sigma (x)$ cannot contain concept constants (i.e., constants) or existential restrictions (i.e., terms starting with a function application). This means that $\sigma (x)$ is a conjunction of variables:

where we assume (without loss of generality) that all the variables $z_i^x$ for a fixed $x$ are pairwise distinct. To obtain $\lambda \sigma (x){\approx }_{ℰℒ}x$, the substitution $\lambda$ must thus assign (modulo ${\approx }_{ℰℒ}$) $x$ or $\top$ to the variables $z_i^x$ for all $i,1\le i\le n_x$, and $x$ to at least one of these variables. Let us assume without loss of generality that $\lambda$ assigns $x$ to $z_1^x$ for all $x\in 𝒳$. This implies that $z_1^x\ne z_1^y$ for different elements $x,y$ of $𝒳$.

Since $\mathrm{VRan}(\sigma )\cap \mathrm{Dom}(\theta )=\mathrm{\varnothing }$, we know that $z_i^x\notin \mathrm{Dom}(\theta )$ for all $x\in 𝒳$ and $1\le i\le n_x$. We claim that $z_i^x\in \mathrm{Dom}(\sigma )$ also holds, and thus $z_i^x\in 𝒳$. Otherwise, $\lambda \sigma (z_i^x)=\lambda (z_i^x)\in \{x,\top \}$. However, $\lambda \sigma (z_i^x){\approx }_{ℰℒ}\theta (z_i^x)=z_i^x$. This yields a contradiction unless $z_i^x=x$. But then we also have $z_i^x\in \mathrm{Dom}(\sigma )$ since $x\in \mathrm{Dom}(\sigma )$. We have thus shown that all the variables $z_i^x$ for $x\in 𝒳$ also belong to $𝒳=\mathrm{Dom}(\sigma )\setminus \mathrm{Dom}(\theta )$. Since $z_1^x\ne z_1^y$ for different elements $x,y$ of $𝒳$, this implies that the $z$-variables with index $1$ already “use up” all of $𝒳$, and thus $n_x=1$ holds for all $x\in 𝒳$.

Consequently, $\sigma$ is a $W$-renaming for $W=\mathrm{Dom}(\sigma )\setminus \mathrm{Dom}(\theta )$, where according to Definition 2.11 in [28] a substitution $\tau$ is a $W$-renaming if $\tau (x)$ is a variable for all $x\in W$ and $\tau$ is injective on $W$. Since $\sigma$ is the identity on $V\setminus \mathrm{Dom}(\sigma )$ and elements of $\mathrm{Dom}(\sigma )\setminus \mathrm{Dom}(\theta )$ are mapped to $\mathrm{Dom}(\sigma )\setminus \mathrm{Dom}(\theta )$ by $\sigma$, the substitution $\sigma$ is also a $W$-renaming for $W=V\setminus \mathrm{Dom}(\theta )$. By Lemma 2.12 in [28], there is a permutation $\pi$ that coincides with $\sigma$ on $W=V\setminus \mathrm{Dom}(\theta )$. Let ${\sigma }^{\prime }:={\pi }^{-1}\sigma$. Then ${\sigma }^{\prime }{\sim }_{\mathrm{\varnothing }}^V\sigma$, and thus also ${\sigma }^{\prime }{\sim }_{ℰℒ}^V\sigma$. In addition, for all $x\notin \mathrm{Dom}(\theta )$ we have ${\sigma }^{\prime }(x)={\pi }^{-1}\sigma (x)=x$, which yields $x\notin \mathrm{Dom}({\sigma }^{\prime })$. This shows that $\mathrm{Dom}({\sigma }^{\prime })\subseteq \mathrm{Dom}(\theta )$. $◀$

This lemma together with the next result shows that, up to equivalence, we can bound the variables occurring in more general substitutions by the substitutions they have as instance.

Let $\lambda$ be such that $\lambda \sigma {\approx }_{ℰℒ}\theta$. Assume that $z\in \mathrm{VRan}(\sigma )$, but $z\notin \mathrm{Dom}(\theta )\cup \mathrm{VRan}(\theta )$. Then $z\notin \mathrm{Dom}(\sigma )$, and thus $\lambda (z)=\lambda \sigma (z){\approx }_{ℰℒ}\theta (z)=z$. However, since $z\in \mathrm{VRan}(\sigma )$, there is a variable $x\in \mathrm{Dom}(\sigma )$ such that $\sigma (x)$ contains $z$. Then $x\in \mathrm{Dom}(\theta )$, and thus all variables occurring in $\theta (x)$ belong to $\mathrm{VRan}(\theta )$. Since $\lambda \sigma (x){\approx }_{ℰℒ}\theta (x)$, this means that $z\in \mathrm{VRan}(\theta )$, which contradicts our assumptions on $z$. $◀$