ch:efficient-unification: ch:efficient-unification

Decomposition of the root pair first equates the two $F$-nodes and then adds $$x\sim G(y),G(a)\sim y.$$ The quotient therefore has one $F$-class, one class containing $x$ and $G(y)$, one class containing $y$ and $G(a)$, and the class of $a$. Both mixed classes have one rigid representative, so the quotient is homogeneous. Its nonconstant arcs run from the $x/G(y)$-class to the $y/G(a)$-class and then to the $a$-class; hence it is acyclic. Reading the rigid recipes gives $$x\mapsto G(y),y\mapsto G(a).$$

After replacing the second root by $F(G(y),x)$, propagation gives $x\sim G(y)$ and $G(a)\sim x$. The two $G$-nodes in this class force $y\sim a$. The quotient remains homogeneous and acyclic, and one triangular MGU is $$y\mapsto a,x\mapsto G(a).$$

The first root class contains the two $H$-nodes. Deleting it creates $$x\sim F(a),F(y)\sim F(a).$$ The maximally shared input has one node for the two printed occurrences of $F(a)$. Consequently the two new links form the single live root class $\{x,F(y),F(a)\}$. Its transition records $x\mapsto F(a)$ and, from the two rigid $F$-nodes, creates the child link $y\sim a$. The second and final root-class transition records $y\mapsto a$. The output $$x\mapsto F(a),y\mapsto a$$ is triangular. Unfolding sends both roots to $H(F(a),F(a))$, which verifies the input equation.

Choose one of the $k$ rigid $q$-ary nodes as representative. Each of the other $k-1$ nodes contributes one equality at each of its $q$ child positions, so the transition creates $q(k-1)$ links. Charge the link from position $j$ of nonrepresentative node $s$ to the unique outgoing arc $(s,s[j])$. The pair $(s,j)$ recovers the charged arc, so the charge is injective.

A node is deleted once. Consequently an outgoing arc is charged only in the transition that deletes its source. Summing over classes bounds all generated links by the input child arcs. Node visits, parent-cursor advances, incident-link advances, stack operations, and bindings likewise admit one constant charge per stored node, arc, link, or variable. Restarting an incident-link cursor after each merge destroys the last claim: a list prefix can then be rescanned after every newly discovered class member, producing quadratic work on a linear-size star of links.

For $x\doteq f(x)$, the linked class contains the flexible node $x$ and the rigid node $f(x)$. With the completion mark inside the $s\ne r$ branch, the rigid representative $r$ remains $\mathsf{owner}=r,\mathsf{Complete}=\mathsf{ff}$ while its parent dependency is followed. The traversal reaches $x$, whose parent is the unfinished representative, and reports the quotient self-cycle. With the mark after the branch, the state instead becomes $\mathsf{owner}(r)=r,\mathsf{Complete}(r)=\mathsf{tt}$ before that revisit. The revisit is skipped and the cyclic recipe $x\mapsto f(x)$ escapes to post-processing.

For $x\doteq f(y)$ and $y\doteq g(x)$, the first link class records $x$ with $f(y)$, and the second records $y$ with $g(x)$. Following the parent of $y$ enters the first unfinished class; following the parent of $x$ returns to the second unfinished class. Thus the corrected procedure first revisits whichever of these two classes was entered first under the implementation’s fixed parent order. The certificate is the two-class quotient cycle $$[x=f(y)]⟶[y=g(x)]⟶[x=f(y)].$$

Maximal sharing uses one node for each of $x,y,z,a,G(a)$, one node for each occurring $H$-recipe, and the two root $F$-nodes. Deleting the root class creates $$x\sim H(z,a),H(y,a)\sim H(G(a),a),y\sim G(a).$$ The first mixed class records $x\mapsto H(z,a)$. Decomposing the two $H$-nodes adds $y\sim G(a)$ and the reflexive link $a\sim a$. The remaining mixed class records $y\mapsto G(a)$; $z$ remains a variable-only quotient parameter. Hence $$S=(x\mapsto H(z,a),y\mapsto G(a)).$$ Every unifier $\theta$ must give $y$ the tree $G(a)$, by rigid injectivity, and must give $x$ the tree $H(\theta (z),a)$. Define $\delta (z)=\theta (z)$. Then $\theta (y)=\delta (S(y))$ and $\theta (x)=\delta (S(x))$; the equation for $z$ is immediate. Thus $\theta =\delta \circ S$ on all input variables.

Use $$F(x)\doteq G(x),x\doteq F(x),x\doteq F(y),y\doteq G(z),z\doteq H(x).$$ The first problem fails in its initial root class because it contains unequal rigid heads $F$ and $G$. A common tree would have both heads, contradicting constructor disjointness. The second problem’s quotient has a self-loop from the class $[x,F(x)]$ to itself. If its tree had height $h$, equality with the proper $F$-subtree would require .

The third problem produces three quotient classes with strict child edges $[x]\to [y]\to [z]\to [x]$. If their unfolded finite-tree heights are $h_x,h_y,h_z$, the three equations imply , an impossible strict cycle. The failure becomes detectable when the last link closes that quotient cycle; no finite-tree substitution can remove it.

Store the recipes $$x_0\mapsto a,x_i\mapsto f(x_{i-1},x_{i-1})(1\le i\le n)$$ once each. This representation has $n+1$ bindings and $2n$ child pointers. To read the root of $x_n$, inspect its recipe. To follow a chosen leaf, read one of the two equal child pointers at each $f$-recipe; after $n$ pointer steps the traversal reaches $a$, so the cost is $O(n)$.

The expanded tree has $2^n$ distinct leaf positions. Any enumeration that emits each position performs at least one output action per position and therefore takes $\mathrm{\Omega }(2^n)$ time. The linear theorem constructs the recipe graph and triangular bindings. It does not claim to enumerate the expanded tree, so the two bounds concern different outputs.