next up previous contents
Next: Signature files Up: ALE Data Structure Previous: Path Compression   Contents


Unification Algorithm

[User's Manual]
[Code]
ALE uses the Martelli-Montanari algorithm, which is a variation of the union algorithm for union-find data structures. The Martelli-Montanari algorithm operates on a finite set of equations

\begin{displaymath}E = \{s_1=t_1,\ldots,s_n=t_n\}\end{displaymath}

and a substitution $\theta$. Initially $E=\{s=t\}$, where $s$ and $t$ are the terms to be unified, and $\theta=\emptyset$. Then the algorithm chooses from $E$ an arbitrary equation and performs acts according to the following rules:

  Equation from $E$ Action
1 $f(s_1,\ldots,s_n)=f(t_1,\ldots,t_n)$ replace by the equations $s_1=t_1,\ldots,s_n=t_n$
2 $f(s_1,\ldots,s_n)=g(t_1,\ldots,t_n)$ fail
3 $X=X$ delete equation
4 $X=t$ or $t=X$ where $X$ does not occur in $t$ add $X\longleftarrow t$ to $\theta$, apply the substitution $\{X\longleftarrow t\}$ to $E$ and the term in $\theta$
5 $X=t$ or $t=X$ where $X$ occurs in $t$ and $X\neq t$ fail
The above procedure is repeated until $E$ becomes empty, or the procedure fails.

Feature structure unification in ALE is done by ud/2 predicate, which first dereferences the two feature structures to be unified getting the most recent term encoding of the feature structure together with its tag, and then it runs the Martelli-Montanari algorithm on the term encodings.


next up previous contents
Next: Signature files Up: ALE Data Structure Previous: Path Compression   Contents
TRALE Reference Manual