Efficient First-Order Unification

Proof. Suppose $\theta$ is a unifier. Put $r{\sim }_{\theta }s$ when $U_{\theta }(r)=U_{\theta }(s)$. Equality of rigid trees gives equal heads and equal corresponding subtrees. If the quotient had a cycle, the finite tree naming one class on that cycle would equal one of its proper subtrees, which finite-tree height forbids. Hence ${\sim }_{\theta }$ is valid.

Conversely, let $\sim$ be valid. Topologically order its quotient from children to parents. Give each variable-only class $C$ a fresh parameter $z_C$. Define a tree $T_C$ by Homogeneity makes the second line independent of $r$, and acyclicity makes the recursion finite. The assignment $x\mapsto T_{[x]}$ makes equivalent nodes unfold equally, hence solves every distinguished pair.

Finally, every valid relation containing the input pairs must contain every pair forced by equivalence and corresponding-child propagation. Their least closure is therefore contained in every valid relation. If that closure had a clash or quotient cycle, every extension would retain it; since a valid extension exists, the least closure is itself valid and is unique. ◻

Proof. Let $R$ be the selected class. Since its nodes have no live parents, their only remaining semantic obligations are the links within $R$. If $R$ is variable-only, the equations $s=r$ for $s\in R\setminus \{r\}$ are exactly the recorded bindings. If $R$ contains rigid nodes, homogeneity gives one common label $f$. Rigid injectivity gives, in both directions, $$f(t_1,\dots ,t_k)=f(u_1,\dots ,u_k)⟺t_1=u_1,\dots ,t_k=u_k.$$ Thus replacing equality of two nodes in $R$ by the child links preserves exactly the solutions. A flexible member must equal the chosen rigid recipe, which is exactly its recorded binding. This proves the first two clauses and also shows why a head clash has no solution.

For the last clause, order quotient classes from parents to children. A maximal class in an acyclic quotient has no incoming child arc. It also has no arc internal to the class, since that would be a quotient self-cycle. Every node in it is therefore a live root. Conversely, a finite quotient with no maximal class has a directed cycle. Induction over transitions now maintains the homogeneous-and-acyclic closure invariant until success, or exposes the first clash or cycle that prevents it. ◻

Proof. Each transition deletes at least one live node, so there are at most $|V(G)|$ transitions. A clash is nonunifiability by rigid-head disjointness. A cycle is nonunifiability by lemma 113.3, lemma 113.5. If the algorithm succeeds, repeated use of lemma 113.5 shows that its bindings solve exactly the original equations.

A flexible node is shared and deleted once, so it is bound at most once. In a rigid class, a right-hand child of the selected root class cannot belong to that class: it has a live parent there and would make the class non-root. Its class is therefore deleted later. In a variable-only class, every nonrepresentative member is bound directly to the chosen representative; that representative receives no binding and is the class parameter in the compact substitution. The bindings are therefore triangular by root-class deletion order, with one parameter at each variable-only leaf class.

For most-generality, take the successful least valid quotient. In each variable-only class $C$, identify the semantic parameter $z_C$ from the proof of lemma 113.3 with the chosen unbound input representative $r_C$ of the operational substitution $S$. Any unifier $\theta$ gives one common tree to all variables of $C$; define $\delta (r_C)$ to be that tree. Induction along the quotient’s child-before-parent topological order gives $\theta (x)=\delta (S(x))$ for every input variable $x$. This is the required factorization. ◻

Proof. At the moment the incident links of $s$ are inspected, every live parent has first been finished and deleted. Thus every node accumulated under owner $r$ is a root when the class is processed. Consuming links computes exactly their connected component. Equal rigid labels generate exactly the child links of the root-class transition; variables generate exactly its bindings.

If recursion encounters a node already owned by a different unfinished invocation, or re-enters the invocation whose owner is $r$, following parent calls and owner links back to that node exhibits a directed cycle in the link quotient. If no such encounter occurs, the stack exhausts the whole root class and deletion implements its transition. Finally, every nonempty acyclic live quotient has a root class by lemma 113.5; the global scan or a parent call reaches one of its nodes. Induction on the number of live nodes gives eventual scheduling of every transition. ◻

Proof. Charge a global-list visit and stack work to its node. Charge a parent-list cursor advance to the child arc it passes, including advances past deleted parents. Charge consuming a link to that link. When a class contains $k$ rigid nodes of arity $q$, it creates $q(k-1)$ child links; charge them to the $q(k-1)$ outgoing arcs of the nonrepresentative rigid nodes deleted in that class. Thus the number of generated links is at most the number of input child arcs, and no node, arc, or link receives more than a constant number of charges. Output bindings are node/recipe pointers and add constant space per bound variable. Correctness and the MGU property follow from theorem 113.6, lemma 113.8. ◻

Proof. The shared input has one variable node $x$ and one rigid node $f(x)$. Linking the roots puts them in one unfinished class. The rigid node has $x$ as a child, while the unique occurrence of $x$ is also the flexible member of that class. With the mark inside the $s\ne r$ branch, the representative remains unfinished until its class stack empties. Following the parent edge from $x$ therefore revisits that unfinished class, which is the quotient self-cycle required for the occurs-check rejection.

With the mark after the branch, the invocation may mark $r$ complete before the revisit. The revisit is skipped as completed, so the procedure emits the cyclic recipe $x\mapsto f(x)$. Expanding that recipe asks again for the expansion of $x$ and has no finite result. Thus the misplaced assignment changes a required rejection into a nonterminating post-processing calculation. Motroi and Ciobâcă give this trace and place the assignment inside the branch in their corrected Figure 7. ◻

Proof. Let $L_n$ and $N_n$ be the numbers of leaves and total nodes in the expanded image of $x_n$. The base equation gives $L_0=N_0=1$. Each successor equation duplicates the preceding tree beneath one new $F$-node, so $$L_{n+1}=2L_n,N_{n+1}=1+2N_n.$$ Induction gives $L_n=2^n$ and $N_n=2^{n+1}-1$. The compact representation stores one binding and two pointers per successor equation, hence has linear size. ◻