LARA

Unification

Unification is the process of solving equations in term algebra, which is the algebra of ground terms, with functions defined as in the Ground Terms section of proof of Herbrand theorem.

The solution process is essentially variable elimination, based on two main properties

  • equation $f(t_1,\ldots,t_n) \doteq f(s_1,\ldots,s_n)$
  • equation $f(t_1,\ldots,t_n) \doteq g(s_1,\ldots,s_m)$ where $f \neq g$
  • equation $x \doteq t(x)$ where $t$ is a term containing $x$ but not identical to $x$

Examples

First-order language:

  • $R$ - binary relation symbol
  • $f$ - binary function symbol
  • $a,b,c$ - constants
  • $x,y,z,u,v,w$ - variables

Example 1

\begin{equation*} R(x,f(x,y)) \doteq R(f(a,v),f(f(u,b),f(u,u))) \end{equation*}

Example 2

\begin{equation*} R(x,f(x,x)) \doteq R(f(a,v),f(f(u,b),f(u,u))) \end{equation*}

Example 3

\begin{equation*} R(x,f(x,y)) \doteq R(f(u,v),v) \end{equation*}

Definition: Unifier of a set $E$ of syntactic equations is a substitution that makes all equations true.

Definition: Composition $\circ$ of substitutions.

Definition: A renaming is a substitution which is (a total function and) a bijection on the set of all variables.

Lemma: If $\sigma$ is a unifier for $E$ and $\tau$ is a substitution, then $\tau \circ \sigma$ is also a unifier.

A unifier is a solution of equations. mgu is the most general solution.

Definition: A most general unifier for $E$ is a unifier $\sigma$ such that if $\sigma'$ is another unifier, then there exists a substitution $\tau$ such that $\sigma' = \tau \circ \sigma$.

Algorithm

We next sketch an algorithm for computing mgu.

A set of equations is in solved form if it is of the form $\{ x_1 \doteq t_1,\ldots, x_n \doteq t_n \}$ iff variables $x_i$ do not appear in terms $t_j$, that is

\begin{equation*} \{x_1,\ldots,x_n \} \cap (FV(t_1) \cup \ldots FV(t_n)) = \emptyset \end{equation*}

We obtain a solved form in finite time using the non-deterministic algorithm that applies the following rules as long as no clash is reported and as long as the equations are not in solved form.

Orient

Select $t \doteq x$ where t is not x, and replace it with $x \doteq t$.

Delete

Select $x \doteq x$, remove it.

Eliminate

Given $x \doteq t$ where $x$ does not occur in $t$, substitute $x$ with $t$ in all remaining equations.

Occurs Check

Given $x \doteq t$ where $x$ occurs in $t$, report clash.

Decomposition

Given $f(t_1,\ldots,t_n) \doteq f(s_1,\ldots,s_n)$, replace it with $t_1 \doteq s_1,\ldots,t_n \doteq s_n$.

Decomposition Clash

Given $f(t_1,\ldots,t_n) \doteq g(s_1,\ldots,s_m)$ for $f$ not $g$, report clash

References