ch:semi-unification: ch:semi-unification

Put $M=\alpha \to \beta$ and $N=\gamma \to \gamma$. The encoding is $$((\alpha \to \beta ),(\alpha \to \beta )){⪯}_{\mathsf{su}}((\alpha \to \beta ),(\gamma \to \gamma )).$$ The substitution $S=[\gamma /\alpha ,\gamma /\beta ]$ is a most general unifier, up to renaming of $\gamma$. After applying $S$, both sides of the encoded inequality are the pair $((\gamma \to \gamma ),(\gamma \to \gamma ))$, so the identity matcher replays it. Conversely, decomposition of any replay equates the two images, hence gives a unifier of the original equation.

Suppose $S,R$ replayed the inequality and put $A=S(\alpha )$, $B=S(\beta )$. Its left side after both substitutions is $(R(A)\to R(B))\to R(A)$, whereas the right side is $A$. Therefore a contradiction. The last inequality holds because a substitution on finite first-order trees retains every constructor node and replaces every variable leaf by a nonempty finite tree. Infinite regular trees do not support this natural-number node count, which is where finiteness is used.

Under monomorphic recursion, let the one type of $f$ be $\delta$. The whole body requires $\delta =\alpha \to \gamma$, while the recursive occurrence $f(\lambda y.x)$ requires $\delta =(\beta \to \alpha )\to \gamma$. Decomposition yields $\alpha =\beta \to \alpha$; its right side contains $\alpha$, so the occurs check rejects it.

Take $S=[\gamma /\beta ]$ and $R=[\gamma /\alpha ]$. The equation becomes $\gamma =\gamma$, and the inequality replays as $R(\alpha \to \alpha )=\gamma \to \gamma$. For any semi-unifier, the equation clause is checked before any local matcher and states $S(\beta )=S(\gamma )$. A matcher belongs only to its inequality and cannot repair an equation, so this equality is necessarily a restriction on the shared outer substitution.

Encode every equation $M\doteq N$ as $(M,M){⪯}_{\mathsf{su}}(M,N)$. Any unifier $S$ semi-unifies all encodings with identity matchers. Conversely, decomposition of each encoded replay gives $S(M)=S(N)$, so the outer substitution is a unifier. The first two FO-Fix inequalities mutually match ${\tau }_x$ and ${\tau }_b$ while protecting $\overline{\rho }$; by lemma 5.9 they express equality of the two generalized schemes. The third premise $({\tau }_b,\overline{\rho }){⪯}_{\mathsf{su}}(\tau ,\overline{\rho })$ is the genuine one-way inequality that instantiates the whole fix expression. It remains when $\mathsf{let}$ is deleted, because it is generated by the recursive binder itself.

Write the annotation as $\sigma =\mathrm{\forall }\overline{\alpha }.\tau$. Replace $\overline{\alpha }$ in the body target by fresh rigid constants $\overline{\kappa }$ and check the body against $\tau [\overline{\kappa }/\overline{\alpha }]$. The free type variables of the ambient environment are rigid as well. Keep the recursive assumption as the written scheme $\sigma$; at each recursive occurrence replace its prefix by fresh flexible variables and generate the ordinary application and abstraction equations. Unification may solve only flexible variables. It rejects an equation that binds a ${\kappa }_i$ or an ambient rigid variable, and its final substitution may not place a ${\kappa }_i$ in any type whose scope extends outside the checked body.

If the checker succeeds, replace each ${\kappa }_i$ by ${\alpha }_i$ in the body derivation. Every recursive leaf is an instance of the written scheme, the rigid target is exactly its body monotype, and generalizing the ${\alpha }_i$ reconstructs the annotated MM-Fix premise. This proves soundness by rule induction. Conversely, alpha-rename the prefix of an annotated derivation, replace its bound variables by fresh rigid constants, and read the flexible instantiations from the recursive leaves. They solve the generated equations without binding or escaping a rigid constant; unification completeness therefore makes the checker accept.

Rigidity is necessary. Checking $\lambda f.\lambda x.fx$ against $\mathrm{\forall }a.a\to a$ with $a$ flexible would solve $a$ as an arrow and accept, although the term’s principal type is $(b\to c)\to (b\to c)$ and it has no such universal type. The rigid checker rejects the attempted arrow equation for ${\kappa }_a$. The algorithm is finite for a supplied annotation. Searching for an annotation quantifies over all finite schemes and is the inference problem excluded by corollary 5.27.