Syntactic Unification Algorithm

The syntactic unification algorithm is a recursive algorithm that returns the most general unifier of two logical predicates, if it exists.

Process

Inputs: $S, T$ , two logical predicate formulae

Initialise the set $E$ of equations and add the equality (potentially as a tuple) $S = T$ to it.
Repeat the following continuously (while) $E$ contains equations of the forms below, do the associated operation

Form	Meaning	Operation
$f (s_{1}, s_{2}, \dots s_{n}) = f (t_{1}, t_{2}, \dots t_{n})$ where $s_{i}$ and $t_{i}$ are terms and $f$ is a function	Same Function Signature	Decompose into $n$ equations ${s_{1} = t_{1}, s_{2} = t_{2}, \dots s_{n} = t_{n}}$ and add them to $E$
$f (s_{1} \dots s_{n}) = g (t_{1} \dots t_{m})$ where $s_{i}$ and $t_{i}$ are terms $f, g$ are functions $f \neq = g$ OR $n \neq = m$	Different Function Signature	No way of unification, halt/fail
$x = x$ where $x$ is a variable	Redundant Equation	Delete the equation from $E$
$x = f (\dots, x, \dots)$ where $x$ is a variable $f$ is a function containing $x$	Infinite Loop	No way of unification, halt/fail
$c = x$ or $f (\dots) = x$ where $x$ is a variable $f$ is a function $c$ is a constant	Opposite Sides,	Swap the equation ( $x$ on LHS) and replace in $E$
$x = t$ where $x \in / t$ $x$ is a variable $t$ is a term that doesn’t contain or equal $x$	Valid Renaming	Treat as $x \mapsto t$ , apply the renaming to all other equations in $E$

Finally, switch all $=$ to $\mapsto$ to create the final mapping.
Return $E$

Properties

This algorithm always halts, so the problem of syntactic unification is decidable
If the algorithm fails, it guarantees that $S$ and $T$ are non-unifiable
Else, the resultant unifier $E$ is a most general unifier

Time Complexity

Case Scenario	Input Description	Growth Function	Big-O	Notes
Worst			$O (n)$
Average
Best
^time-complexity

Resources

Paper on Unification Algorithm