Actions

Unifiers

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:

 MGU$(M)$
 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'
   else
     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'
     else
       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)))\}$.