From Learning Logic for Computer Science

Unifiers are term substitutions which, when applied, make literals identical. Most general unifiers represent the set of all unifiers of given literals in a concise fashion and can be computed.

Definition Let $\mathcal S$ be a signature and $M$ a set of literals over $\mathcal S$. A term substitution $\sigma$ over $\mathcal S$ is a unifier for $M$ if $L \sigma = L' \sigma$ for all $L, L' \in \sigma$. The set $M$ is said to be unifiable if there exists a unifier for it.

Example The set $\{P(x_0), P(f(x_1))\}$ is unifiable and $\{x_0 \mapsto f(x_1)\}$ and $\{x_0 \mapsto f(a), x_1 \mapsto a\}$ are unifiers. (The second one only if $a$ is an element of the signature considered.) The set $\{P(x_0), P(f(x_0))\}$ is not unifiable.

When substitution is extended to sets of literals, the above definition can be rephrased as follows. A substitution $\sigma$ is a unifier for a set $M$ of literals if $|M\sigma| \leq 1$.

Most general unifiers

Important questions are:

  • How can the set of all unifiers of a given set $M$ be described?
  • Can this set or a represenation of it be computed?

All unifiers can be seen as instances of a single one, which means the set of all unifiers of a given set can easily be described be such a unifier and there are algorithms to compute this (one) most general unifier.

Example In the above example, the unifier $\{x_0 \mapsto f(a), x_1 \mapsto a\}$ can be obtained from the unifier $\{x_0 \mapsto f(x_1)\}$ by composing it with the substitution $\{x_1 \mapsto a\}$. In fact, $\{x_0 \mapsto f(x_1)\}$ is one of the most general unifiers for the given set.

Formal definition

A substitution $\sigma$ is said to be more specific than a substitution $\sigma'$, denoted $\sigma \leq \sigma'$, if there is a substitution $\sigma^*$, such that $x_i \sigma = x_i \sigma'\sigma^*$ for every $i \in \mathbf N$.

Example Continuing the example, $\{x_0 \mapsto f(a), x_1 \mapsto a\} \leq \{x_0 \mapsto f(x_1)\}$. Reason: One can choose $\sigma^* = \{x_1 \mapsto a\}$ in the above definition.

The relation $\leq$ has several simple properties.

Lemma The relation $\leq$ defined on term substitutions is a preorder (reflexive and transitive).

The proof is straightforward.

As a consequence of this lemma, the relation ${\leq} \cap {\geq}$, which is denoted $\equiv$, is an equivalence relation

Lemma Let $\sigma_0$ and $\sigma_1$ be term substitutions. Then $\sigma_0 \equiv \sigma_1$ if, and only if, they are identical up to renaming.

Proof Let $\sigma_0$ and $\sigma_1$ be substitutions.

Clearly, if $\sigma_0$ and $\sigma_1$ are identical up to renaming, then they are equivalent.

For the other direction, assume $\sigma_0 \equiv \sigma_1$. Then there exist substitutions $\sigma_0^*$ and $\sigma_1^*$ such that $x_i \sigma_0 = x_i\sigma_1\sigma_1^*$ and $x_i \sigma_1 = x_i \sigma_0 \sigma_0^*$ for every $i \in \mathbf N$. As a consequence, we have $x_i \sigma_1 = x_i \sigma_0\sigma_0^* = x_i\sigma_1\sigma_1^*\sigma_0^*$ for every $i \in \mathbf N$. So, for every $j$ with $x_j \in \text{range}(x_i\sigma_1)$ the substitution $\sigma_1^*\sigma_0^*$ works as the identity. In other words, $\sigma_1^*$ restricted to these variables is a renaming that works.

Theorem Let $M$ be a finite set of literals. If $M$ is unifiable, then there is a greatest unifier. Such a unifier is called a most general unifier of $M$.

One way to prove this is to show that algorithm below is correct. It computes a most general unifier in an iterative fashion.

Example Let $M = \{P(x_0), P(f(x_1))\}$ be as above. Then $M$ is unifiable and $\{x_0 \mapsto f(x_1)\}$ and $\{x_0 \mapsto f(x_0), x_1 \mapsto x_0\}$ are most general unifiers, but $\{x_0 \mapsto f(a), x_1 \mapsto a\}$ is not.

Since renaming variables preserves the property of being a greatest unifier, there is not 'the' greatest unifier. The set of all greatest unifiers of a set $M$ of literals over the same signature is denoted $\text{mgu}(M)$.

Computing a most general unifier (Unification)

There are several algorithms for computing most general unifiers. A simple one works as described below. It can be used to show the existence of most general unifiers.

Recall that an address in a tree with ordered siblings is a sequence of natural numbers encoding a path from the root to a vertex: the empty sequence, $\langle \rangle$, denotes the root itself; the sequence $\langle 1\rangle$ denotes the second child of the root, the sequence $\langle 1,0\rangle$ denotes the the first child of the second child of the root. For a given address $\alpha$ and tree $t$, we write $t \downarrow \alpha$ for the tree rooted at the vertex denoted by $\alpha$.

Example Let $L = P(f(g(x_3), g(g(a))))$ and $\alpha = \langle 0,1,0\rangle$. Then $L \downarrow \alpha$ denotes the term $g(a)$. Similarly, $L \downarrow \langle \rangle = L$ for every literal $L$.

The crucial notion in this algorithm is the notion of a disagreement between literals $L$ and $L'$.

Definition Let $L$ and $L'$ be positive literals. An address $\alpha$ of $L$ and $L'$ is a disagreement for $L$ and $L'$ if $L \downarrow \alpha = x_i$ for some $i \in \mathbf N$ and $L' \downarrow \alpha \neq x_i$.

Note that this definition is not symmetric. Note also that it might be reasonable to require that in $L$ and $L'$ the paths determined by $\alpha$ have the same labels.

Example Consider the positive literals $P(a, f(x_2, g(x_1), x_1))$ and $P(x_3, f(x_2, h(x_5), h(x_2)))$. There is one disagreement of $L$ and $L'$, namely $\langle 1, 2 \rangle$, and there is one disagreement of $L'$ and $L$, namely $\langle 0 \rangle$.

The following algorithm is a simple mgu-finder:

 Precondition: $M$ is a finite set of positive literals.
 let $N = M$
 let $\sigma = \emptyset$
 while $|N| > 1$
   if there is no disagreement between literals in $N$
     return 'not unifiable'
     let $\alpha$ be a disagreement for $L, L' \in N$
     assume $x_i = L\downarrow \alpha$
     if $x_i \in \text{vars}(L' \downarrow \alpha)$
       return 'not unifiable'
       let $\sigma = \sigma\{x_i \mapsto L\downarrow \alpha\}$
       let $N = N \sigma$
  return $\sigma$
  Postcondition: if $M$ is unifiable, then return is a most general unifier of $M$
                 if $M$ is not unifiable, then return = 'not unifiable'

Example Let $M = \{P(x_0, f(x_0)), P(f(x_1), x_2), P(f(f(a)), f(f(f(a))))\}$. The following describes a possible run of the above algorithm on $M$:

  1. $\sigma = \emptyset$, $N = \{P(x_0, f(x_0)), P(f(x_1), x_2), P(f(f(a)), f(f(f(a))))\}$.
  2. $P(x_0, f(x_0), x_0)$ and $P(f(x_1), x_1, )$ disagree at $\langle 0$.
  3. $\sigma = \{x_0 \mapsto f(x_1)\}$, $N = \{P(f(x_1), f(f(x_1)), x_0), P(f(x_1), x_2), P(f(f(a)), f(f(f(a))))\}$.
  4. $P(f(x_1), x_2)$ and $P(f(x_1), f(f(x_1)))$ disagree at $\langle 1\rangle$.
  5. $\sigma = \{x_0 \mapsto f(x_1)\}\{x_2 \mapsto f(f(x_1))\} = \{x_0 \mapsto f(x_1), x_2 \mapsto f(f(x_1))\}$, $N = \{P(f(x_1), f(f(x_1))), P(f(f(a)), f(f(f(a))))\}$.
  6. $P(f(x_1), f(f(x_1)))$ and $P(f(f(a)), f(f(f(a))))$ disagree at $\langle 0, 0 \rangle$.
  7. $\sigma = \{x_0 \mapsto f(x_1), x_2 \mapsto f(f(x_1))\}\{x_1 \mapsto f(a)\} = \{x_0 \mapsto f(f(a)), x_2 \mapsto f(f(f(a)))\}$, $N = \{P(f(f(a)), f(f(f(a))))\}$.
  8. return $\{x_0 \mapsto f(f(a)), x_2 \mapsto f(f(f(a)))\}$.