# 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$:

- $\sigma = \emptyset$, $N = \{P(x_0, f(x_0)), P(f(x_1), x_2), P(f(f(a)), f(f(f(a))))\}$.
- $P(x_0, f(x_0), x_0)$ and $P(f(x_1), x_1, )$ disagree at $\langle 0$.
- $\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))))\}$.
- $P(f(x_1), x_2)$ and $P(f(x_1), f(f(x_1)))$ disagree at $\langle 1\rangle$.
- $\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))))\}$.
- $P(f(x_1), f(f(x_1)))$ and $P(f(f(a)), f(f(f(a))))$ disagree at $\langle 0, 0 \rangle$.
- $\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))))\}$.
- return $\{x_0 \mapsto f(f(a)), x_2 \mapsto f(f(f(a)))\}$.