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

$$E = \{s_1=t_1,\ldots,s_n=t_n\}$$

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.