Semi-Unification and Polymorphic Recursion

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Extend the pure term grammar of chapter 3 by $$e::=\cdots \mid \mathsf{fix}f.e.$$ The constructor $\mathsf{fix}f.e$ binds $f$ in $e$. Terms are identified up to alpha-renaming of that binder, and substitution is the capture-avoiding substitution of definition 1.58 with the new clause $$(\mathsf{fix}f.e)[u/x]=\mathsf{fix}f.(e[u/x])(f\ne x,f\notin \mathrm{FV}(u)),$$ after alpha-renaming $f$ when the freshness condition fails. Operationally, one step unfolds one copy: $$\mathsf{fix}f.e⟶e[\mathsf{fix}f.e/f].$$ The monomorphic-recursion baseline assigns one monotype $\tau$ to the binder and requires the body to have that same monotype: $$\frac{\mathrm{\Gamma },f:\tau ⊢e:\tau }{\mathrm{\Gamma }⊢\mathsf{fix}f.e:\tau }\mathrm{Mono}-\mathrm{Fix}.$$

Now consider $$\mathsf{fix}f.\lambda x.f(\lambda y.x).$$ Choose fresh type variables $\alpha ,\beta ,\gamma$. If the argument of the outer abstraction has type $\alpha$, then $\lambda y.x$ has type $\beta \to \alpha$. The recursive occurrence therefore needs an instance $$f:(\beta \to \alpha )\to \gamma$$ of $\mathrm{\forall }\zeta \eta .\zeta \to \eta$; polymorphic recursion will assign this scheme to $f$. Under monomorphic recursion, the whole body $\lambda x.f(\lambda y.x)$ has type $\alpha \to \gamma$, so Mono-Fix assigns $f$ that same type. Equating it with the occurrence type and decomposing the outer arrows gives $$\alpha \to \gamma =(\beta \to \alpha )\to \gamma ⟹\alpha =\beta \to \alpha ,$$ which fails the occurs check: a finite first-order type cannot equal a type containing itself as a proper subtree. The missing operation is not another equality solver: each recursive occurrence must be allowed a separate instance of the scheme assigned to the definition. Equation (5.1) also shows that the term diverges when it is applied; typability here is a static property, not a termination claim.

One outer substitution and many matchers

Fix the arrow signature with a countably infinite set $\mathcal{V}$ of type variables. Its first-order terms are $$M,N::=\alpha \mid M\to N,\alpha \in \mathcal{V}.$$ A finite substitution $S$ maps finitely many variables to arrow terms, fixes every other variable, and extends homomorphically, so $S(M\to N)=S(M)\to S(N)$.

Thus $\alpha {⪯}_{\mathsf{su}}\beta \to \beta$, witnessed by $R=[\beta \to \beta /\alpha ]$. In contrast, $\alpha \to \alpha {⪯}_{\mathsf{su}}\beta \to \gamma$ holds exactly when $\beta =\gamma$: because equal arrow trees have equal left and right children, decomposition gives both $R(\alpha )=\beta$ and $R(\alpha )=\gamma$. Conversely, if $\beta =\gamma$, the matcher $[\beta /\alpha ]$ witnesses the relation.

The distinction between $S$ and the $R_i$ is load-bearing. The problem $$\{\alpha {⪯}_{\mathsf{su}}\alpha \to \alpha ,\alpha {⪯}_{\mathsf{su}}\alpha \to (\alpha \to \alpha )\}$$ has the outer solution $S=\mathsf{id}$. Its first matcher sends $\alpha$ to $\alpha \to \alpha$; its second matcher sends $\alpha$ to $\alpha \to (\alpha \to \alpha )$. Requiring one matcher for the whole family would reject equation 5.4 and would define a different problem.

Unification is recovered by forcing a matcher to give the same result in two positions.

Proof of Proposition 5.3 — Equation encoding

Proof. If $S(M)=S(N)$, the identity matcher witnesses the right side of equation 5.5. Conversely, let $R$ witness the right side. Decomposition gives $$R(S(M))=S(M),R(S(M))=S(N).$$ Transitivity of syntactic equality gives $S(M)=S(N)$. ◻

The next failure is smaller than the undecidability construction, but it shows why an occurs check is still present inside the larger problem.

Proof of Lemma 5.4 — Finite-tree obstruction

Proof. Suppose $S$ and $R$ satisfied $R(S(\alpha )\to S(\alpha ))=S(\alpha )$. Homomorphic extension gives $$R(S(\alpha )\to S(\alpha ))=R(S(\alpha ))\to R(S(\alpha )).$$ Define the node count by $|\alpha |=1$ and $|P\to Q|=1+|P|+|Q|$. The assumed equality and equation 5.6 give $$|S(\alpha )|=1+2|R(S(\alpha ))|.$$ Every variable leaf of $S(\alpha )$ is replaced by a nonempty term, and every arrow node is retained. Hence $|R(S(\alpha ))|\ge |S(\alpha )|$. Equation 5.7 would imply $|S(\alpha )|\ge 1+2|S(\alpha )|$, which is impossible in $\mathbb{N}$. ◻

The Milner–Mycroft calculus

The complete programming language is the pure extended lambda calculus: $$e::=x\mid \lambda x.e\mid ee\mid \mathsf{let}x=e\mathsf{in}e\mid \mathsf{fix}x.e.$$ The binders and operational clause for $\mathsf{fix}$ are those stated at the chapter opening. Constants can be represented by variables in a fixed global environment. Monotypes and predicative schemes are $$\tau ::=\alpha \mid \tau \to \tau ,\sigma ::=\tau \mid \mathrm{\forall }\alpha .\sigma .$$ Quantifiers occur only in the prefix of a scheme and range over monotypes. For a scheme $\sigma =\mathrm{\forall }\overline{\alpha }.\tau$, write $\sigma \succcurlyeq {\tau }^{\prime }$ when ${\tau }^{\prime }=\tau [\overline{\nu }/\overline{\alpha }]$ for a positionwise vector of monotypes $\overline{\nu }$.

The opening term has a complete finite derivation. Put $\sigma =\mathrm{\forall }\zeta \eta .\zeta \to \eta$ and ${\mathrm{\Gamma }}_f=f:\sigma$ and $\mathrm{\Delta }={\mathrm{\Gamma }}_f,x:\alpha$. The quantified variables $\zeta ,\eta$ are distinct from the free variables $\alpha ,\beta ,\gamma$. Substituting $\beta \to \alpha$ for $\zeta$ and $\gamma$ for $\eta$ witnesses the instance used below. Its application subderivation is $${\mathcal{D}}_{\mathrm{app}}=\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{(f:\sigma )\in \mathrm{\Delta }}{\mathrm{\Delta }{⊢}_{\mathsf{MM}}f:\sigma }}\mathrm{Var}\\ \sigma \succcurlyeq (\beta \to \alpha )\to \gamma \end{array}}{\mathrm{\Delta }{⊢}_{\mathsf{MM}}f:(\beta \to \alpha )\to \gamma }}\mathrm{Inst}\\ {\displaystyle \frac{{\displaystyle \frac{(x:\alpha )\in (\mathrm{\Delta },y:\beta )}{\mathrm{\Delta },y:\beta {⊢}_{\mathsf{MM}}x:\alpha }}\mathrm{Var}}{\mathrm{\Delta }{⊢}_{\mathsf{MM}}\lambda y.x:\beta \to \alpha }}\mathrm{Lam}\end{array}}{\mathrm{\Delta }{⊢}_{\mathsf{MM}}f(\lambda y.x):\gamma }\mathrm{App}.$$ Recall that $\mathrm{ftv}({\mathrm{\Gamma }}_f)$ is the set of type variables free in the schemes of ${\mathrm{\Gamma }}_f$. Since $\sigma$ is closed, $\mathrm{ftv}({\mathrm{\Gamma }}_f)=\varnothing$, so both generalization side conditions below hold. The second Gen conclusion is $\mathrm{\forall }\alpha .\mathrm{\forall }\gamma .\alpha \to \gamma$, which is $\sigma$ up to alpha-equivalence. Using the application subtree, the complete outer derivation is $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{{\mathcal{D}}_{\mathrm{app}}}{{\mathrm{\Gamma }}_f{⊢}_{\mathsf{MM}}\lambda x.f(\lambda y.x):\alpha \to \gamma }}\mathrm{Lam}\\ \gamma \notin \mathrm{ftv}({\mathrm{\Gamma }}_f)\end{array}}{{\mathrm{\Gamma }}_f{⊢}_{\mathsf{MM}}\lambda x.f(\lambda y.x):\mathrm{\forall }\gamma .\alpha \to \gamma }}\mathrm{Gen}\\ \alpha \notin \mathrm{ftv}({\mathrm{\Gamma }}_f)\end{array}}{{\mathrm{\Gamma }}_f{⊢}_{\mathsf{MM}}\lambda x.f(\lambda y.x):\sigma }}\mathrm{Gen}}{{⊢}_{\mathsf{MM}}\mathsf{fix}f.\lambda x.f(\lambda y.x):\sigma }\mathrm{MM}-\mathrm{Fix}.$$ The derivation is finite even though the unannotated program diverges when called.

Removing schemes from the constraint judgment

A constraint generator needs to remember which type variables may be instantiated. A simple environment $A$ maps term variables to monotypes. The corresponding MM environment $\mathrm{\Gamma }$ maps the same term variables to schemes; $A$ is obtained by erasing each scheme’s quantifier prefix. The formerly bound variables thereby become free in $A$ and remain available to matchers. The nongeneric variables of $\mathrm{\Gamma }$ are the members of $\mathrm{ftv}(\mathrm{\Gamma })$. Initially, the finite sequence $\overline{\rho }$ contains each such variable $\alpha$ as the variable monotype $\alpha$, in any fixed order. While the derivation enters a lambda body, it appends that binder’s monotype; leaving the body removes it. The protected set is $\bigcup _{\rho \in \overline{\rho }}\mathrm{ftv}(\rho )$. Every other variable of a let- or fix-bound type may be changed by a matcher. Omitting the ambient nongeneric variables would incorrectly permit a monomorphic assumption $x:\alpha$ to be used at the unrelated type $\beta \to \beta$.

If $\overline{\rho }=({\rho }_1,\dots ,{\rho }_k)$, then $(\tau ,\overline{\rho })$ denotes the right-associated arrow tuple $(\tau ,{\rho }_1,\dots ,{\rho }_k)$; when $k=0$, it denotes $\tau$ itself. The notation $(\overline{\rho },\tau )$ appends $\tau$ to that sequence.

The protected side condition can be calculated before stating the rules. Take ${\mathrm{\Gamma }}_f=f:\mathrm{\forall }\delta .\delta \to \gamma$. Erasing its prefix gives $A(f)=\delta \to \gamma$, while its free variable gives the initial protected sequence $\overline{\rho }=(\gamma )$. Using $f$ at the opening’s occurrence type $(\beta \to \alpha )\to \gamma$ requires $$(\delta \to \gamma ,\gamma ){⪯}_{\mathsf{su}}((\beta \to \alpha )\to \gamma ,\gamma ).$$ The matcher $[\beta \to \alpha /\delta ]$ changes the first component and fixes the protected component $\gamma$. Distinct variables $\delta$ and $\alpha$ permit this inequality. Rule Mono-Fix would identify $\delta$, the domain of the recursive function’s assumed type, with $\alpha$, the domain of the outer abstraction, and would impose the occurs-check equation $\alpha =\beta \to \alpha$.

Here is one complete use of the new variable rule. With $A=(f:\delta \to \gamma )$ and protected sequence $(\gamma )$, the calculated matcher above supplies the only nonlookup premise: $$\frac{\begin{array}{c}A(f)=\delta \to \gamma \\ (\delta \to \gamma ,\gamma ){⪯}_{\mathsf{su}}((\beta \to \alpha )\to \gamma ,\gamma )\end{array}}{A;(\gamma ){⊢}_{\mathsf{FO}}f:(\beta \to \alpha )\to \gamma }\mathrm{FO}-\mathrm{Var}.$$

The identity function gives a complete derivation in the syntax-directed judgment: $$\frac{{\displaystyle \frac{(x:\alpha )\succcurlyeq \alpha }{x:\alpha {⊢}_{\mathsf{SD}}x:\alpha }}\mathrm{SD}-\mathrm{Var}}{\varnothing {⊢}_{\mathsf{SD}}\lambda x.x:\alpha \to \alpha }\mathrm{SD}-\mathrm{Abs}.$$

Proof of Theorem 5.8 — Local syntax-directed normalization

Proof. Two transformations are used in the induction. If a type substitution $U$ fixes $\mathrm{ftv}(\mathrm{\Gamma })$, applying $U$ to every displayed monotype in a derivation preserves each rule and its freshness premise. The proof is rule induction; at Gen, rename the quantified variable away from $\mathrm{dom}(U)\cup \mathrm{ftv}(\mathrm{rng}(U))$ before applying the induction hypothesis. Also, replacing an assumption by a scheme with at least the same monotype instances preserves derivability. This is rule induction again; only Var changes, and its old instance remains available.

For the forward direction, strengthen the induction statement by fixing a requested monotype instance of the concluding scheme. Standardize every prefix and the range of the requested instantiation apart. In Var, the requested monotype is an instance of $\mathrm{\Gamma }(x)$, so SD-Var applies. In Inst, compose the displayed instantiation with the requested one. In Gen, substitute the requested monotype for the freshly bound variable; the side condition ensures that this substitution fixes $\mathrm{\Gamma }$.

The Lam case applies the induction hypothesis to the body and then SD-Abs. The App case freshens the private variables of its two premises, invokes both induction hypotheses at the common argument monotype, and uses SD-App. For Let, normalize the bound expression to ${\tau }_1$. The scheme ${\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_1)$ contains every instance supplied by the old bound scheme. Replace the old assumption by this standardized-apart maximal scheme, normalize the body, and apply SD-Let.

For MM-Fix, expose the body monotype ${\tau }_b$ immediately below the final generalizations and instantiations. Standardize its recursive prefix apart, replace the recursive assumption by ${\mathrm{Gen}}_{\mathrm{\Gamma }}({\tau }_b)$, and apply the induction hypothesis to the body. The requested result monotype is an instance of that same scheme, so SD-Fix closes the case. This treats Var, Inst, Gen, Lam, App, Let, and MM-Fix; no rule family is delegated.

For the reverse direction, induct on the syntax-directed derivation. SD-Var expands to Var followed by Inst. The abstraction and application cases use the corresponding MM rules. In SD-Let, apply Gen once for each variable in the displayed maximal prefix before Let. In SD-Fix, generalize the body to $\sigma$, use MM-Fix, and instantiate its result to $\tau$. Alpha-equivalent prefixes are identified by the binding convention. The construction preserves a specified monotype conclusion. ◻

Proof of Lemma 5.9 — Mutual protected matching is renaming

Proof. Let $R(M,P)=(N,P)$ and $Q(N,P)=(M,P)$. A substitution on finite arrow trees never decreases node count: it retains every arrow node and replaces a variable leaf by a nonempty tree. Hence $$|M|\le |N|\le |M|.$$ Both inequalities are equalities. Every variable leaf changed by either matcher is therefore replaced by one variable leaf, never by an arrow. If two distinct leaf classes of $M$ were identified by $R$, the corresponding leaves of $N$ would be identical and $Q$ could not recover their distinct occurrence classes. The same argument with $M,N$ interchanged proves that the leaf-class map is surjective. The resulting bijection preserves the complete occurrence pattern. The tuple equations $R(P)=P=Q(P)$ force it to fix the variables of $P$. A renaming and its inverse prove the converse, and quantifying the variables outside $P$ turns that renaming into alpha-equivalence. ◻

Proof of Lemma 5.10 — Scheme representation

Proof. Rule induction on the syntax-directed derivation proves the forward implication.

In the variable case, write $\mathrm{\Gamma }(x)=\mathrm{\forall }\overline{\alpha }.{\tau }_x$. The MM instance replaces only $\overline{\alpha }$ and fixes every nongeneric variable. The latter variables are exactly those occurring in $\overline{\rho }$. The same replacement therefore witnesses $({\tau }_x,\overline{\rho }){⪯}_{\mathsf{su}}(\tau ,\overline{\rho })$ and derives FO-Var. The ambient free variables already occur in $\overline{\rho }$, and the abstraction case adds its domain type, so subsequent matchers fix every nongeneric variable. The application case turns the final App premise into the equality ${\tau }_1={\tau }_2\to \tau$. At a let, variables free in the inferred type of $e_1$ but absent from $\overline{\rho }$ are precisely the variables generalized by SD-Let. At a fix, standardize the recursive prefix apart from the body monotype. Their erased monotypes are variants outside $\overline{\rho }$, so lemma 5.9 supplies both protected matchings. The result instance supplies the third protected matching.

For the reverse implication, induct on the first-order derivation. In FO-Var, a witnessing matcher changes no variable of $\overline{\rho }$; quantify the other variables of $A(x)$, apply Inst, and obtain the conclusion type. In FO-Abs, extend the MM environment by the monomorphic domain and apply the induction hypothesis to the body. The equality side condition then permits Lam. The FO-App case applies the two induction hypotheses and App. In FO-Let, generalize exactly the variables of ${\tau }_1$ absent from $\overline{\rho }$ before applying the induction hypothesis to $e_2$. In FO-Fix, mutual protected matching makes the recursive template and body variants by lemma 5.9. Quantify their variables absent from $\overline{\rho }$, identify the resulting schemes up to alpha-renaming, and use SD-Fix; the remaining inequality supplies its result instance. These five cases exhaust the term grammar. ◻

Constraint generation and the forward reduction

Let $V_0$ be the finite set of type-variable names already used in the destination problem. For each syntax-node occurrence $p$ in a term, choose a root type variable $a_p$; for each lambda or fix binder at $p$, choose a binder variable $b_p$. The entire family $\{a_p\}\cup \{b_p\}$ is pairwise distinct and disjoint from $\mathrm{ftv}(A)\cup \mathrm{ftv}(\overline{\rho })$ and from every member of $V_0$. Write $e^p$ when $p$ is the root occurrence of $e$.

Before giving the general recursion, run it on $\lambda x.x$. Let $q$ be the lambda root and $p$ its variable child. The binder has variable $b_q$; the two root variables are $a_q,a_p$. The variable occurrence contributes $$\underset{\begin{array}{c}\text{binder type and}\\ \text{protected binder}\end{array}}{\underbrace{(b_q,b_q)}}{⪯}_{\mathsf{su}}\underset{\begin{array}{c}\text{occurrence root and}\\ \text{same protected binder}\end{array}}{\underbrace{(a_p,b_q)}},$$ and the lambda contributes $a_q\doteq b_q\to a_p$. Thus the generator must remember both the root $q$ and the binder selected by the occurrence at $p$. The procedure $\mathsf{SEI}(A,\overline{\rho },e^p)$ traverses the syntax once and returns $a_p$ with a finite mixed problem.

The construction records equations separately from inequalities. Applying proposition 5.3 converts the result to inequalities only, with a linear increase in size.

The opening term is the smallest useful complete run. Give its fix, abstraction, application, variable, inner abstraction, and inner variable roots the names $p,q,r,s,t,u$, respectively. The generator returns $$\begin{array}{c}(b_p,b_q){⪯}_{\mathsf{su}}(a_s,b_q),(b_q,b_q,b_t){⪯}_{\mathsf{su}}(a_u,b_q,b_t),\\ a_t\doteq b_t\to a_u,a_s\doteq a_t\to a_r,a_q\doteq b_q\to a_r,\\ b_p{⪯}_{\mathsf{su}}{a}_q,a_q{⪯}_{\mathsf{su}}{b}_p,a_q{⪯}_{\mathsf{su}}{a}_p.\end{array}$$

The following outer substitution solves the equations: The first inequality uses $R_s=[\beta \to \alpha /\delta ]$; the second uses the identity; the two recursive variant inequalities use $R_{xb}=[\alpha /\delta ]$ and $R_{bx}=[\delta /\alpha ]$; the result inequality uses the identity. Each matcher fixes its displayed protected components. For example, $$R_s(S(b_p),S(b_q))=((\beta \to \alpha )\to \gamma ,\alpha )=(S(a_s),S(b_q)).$$ The independent variables $\delta$ and $\alpha$ are essential: the two opposite matchers identify their generalized schemes without forcing the recursive template to equal the monomorphic outer-lambda domain.

The same witness gives the complete first-order derivation. With $A(f)=\delta \to \gamma$, let ${\mathcal{D}}_{\mathrm{app}}$ be the following complete application subderivation: $$\frac{\begin{array}{c}{\displaystyle \frac{(\delta \to \gamma ,\alpha ){⪯}_{\mathsf{su}}((\beta \to \alpha )\to \gamma ,\alpha )}{f:\delta \to \gamma ,x:\alpha ;(\alpha ){⊢}_{\mathsf{FO}}f:(\beta \to \alpha )\to \gamma }}\mathrm{FO}-\mathrm{Var}\\ {\displaystyle \frac{{\displaystyle \frac{(\alpha ,\alpha ,\beta ){⪯}_{\mathsf{su}}(\alpha ,\alpha ,\beta )}{f:\delta \to \gamma ,x:\alpha ,y:\beta ;(\alpha ,\beta ){⊢}_{\mathsf{FO}}x:\alpha }}\mathrm{FO}-\mathrm{Var}}{f:\delta \to \gamma ,x:\alpha ;(\alpha ){⊢}_{\mathsf{FO}}\lambda y.x:\beta \to \alpha }}\mathrm{FO}-\mathrm{Abs}\end{array}}{f:\delta \to \gamma ,x:\alpha ;(\alpha ){⊢}_{\mathsf{FO}}f(\lambda y.x):\gamma }\mathrm{FO}-\mathrm{App}.$$ The remaining two rule instances are $$\frac{\begin{array}{c}{\displaystyle \frac{{\mathcal{D}}_{\mathrm{app}}}{f:\delta \to \gamma ;(){⊢}_{\mathsf{FO}}\lambda x.f(\lambda y.x):\alpha \to \gamma }}\mathrm{FO}-\mathrm{Abs}\\ \delta \to \gamma {⪯}_{\mathsf{su}}\alpha \to \gamma \\ \alpha \to \gamma {⪯}_{\mathsf{su}}\delta \to \gamma \\ \alpha \to \gamma {⪯}_{\mathsf{su}}\alpha \to \gamma \end{array}}{\varnothing ;(){⊢}_{\mathsf{FO}}\mathsf{fix}f.\lambda x.f(\lambda y.x):\alpha \to \gamma }\mathrm{FO}-\mathrm{Fix}.$$ Here the three final matchers are $R_{xb}$, $R_{bx}$, and the identity.

Proof of Theorem 5.12 — Constraint characterization

Proof. Proceed by structural induction on $e$ while keeping the same outer substitution $S$ throughout. This formulation avoids combining independently chosen substitutions from sibling subterms.

Variable. The only generated constraint is $(A(x),\overline{\rho }){⪯}_{\mathsf{su}}(a_p,\overline{\rho })$. A first-order variable derivation has exactly that side condition after applying $S$. The generated matcher is therefore equivalent to the premise of FO-Var.

Abstraction. The induction hypothesis identifies the body constraints with $$S(A)[x\mapsto S(b_p)];(S(\overline{\rho }),S(b_p)){⊢}_{\mathsf{FO}}e:S(a_q).$$ The remaining generated equation says $S(a_p)=S(b_p)\to S(a_q)$, exactly the conclusion type of FO-Abs.

Application. The two induction hypotheses use the restrictions of the same $S$ to $E_1$ and $E_2$. The final equation is $S(a_q)=S(a_r)\to S(a_p)$, which is precisely the arrow premise of FO-App. Reading this argument backward proves the converse.

Let. The first induction hypothesis derives $e_1:S(a_q)$. The second derives $e_2:S(a_r)$ under $x:S(a_q)$. Rule FO-Let gives the body type, and $S(a_p)=S(a_r)$ is the remaining generated equation. Conversely, inversion of FO-Let and that equality recovers both subproblem solutions.

Fix. The body induction hypothesis derives $S(A)[x\mapsto S(b_p)];S(\overline{\rho }){⊢}_{\mathsf{FO}}e:S(a_q)$. The three remaining generated inequalities are, in order, the two mutual protected matchings between $S(b_p)$ and $S(a_q)$ and the protected matching from $S(a_q)$ to $S(a_p)$. They are exactly the three side conditions of FO-Fix. Inverting that rule reads the same argument backward.

These five constructor cases establish both directions. For empty $A$ and $\overline{\rho }$, combine this result with lemma 5.10, theorem 5.8 to obtain the final closed-term claim. ◻

The two-node input $\lambda x.x$ gives an exact emission trace. A preliminary scan validates the stream, counts two nodes, one equation, and one inequality, and emits the equation and inequality counts $\mathsf{fr}(1)\mathsf{fr}(1)$. Prefix-tree nodes $0$ and $1$ are the lambda and variable. In the remaining output, each underbrace decodes the framed field above it: The row labels are the decoded clauses $a_0\doteq b_0\to a_1$ and $(b_0,b_0){⪯}_{\mathsf{su}}(a_1,b_0)$. Resolving index $0$ at node $1$ selects the binder at node $0$; no path is stored between the two scans.

Proof of Corollary 5.14 — Forward reduction

Proof. By theorem 5.8, lemma 5.10, theorem 5.12, a closed term is typable exactly when its generated problem has a semi-unifier.

First make one validation pass. Framing lets the transducer advance from one record to the next with an input-position and payload-length counter. It checks constructor arities and binder-index bounds while maintaining the current binder depth. The same pass computes the exact syntax-node count $N$ and the numbers of generated equation and inequality clauses: a variable contributes one inequality clause, a lambda or application one equation clause, a let one equation clause, and a fix three inequality clauses. It emits the latter two counts before the records. Put ${\mathcal{I}}_{-}=\{\alpha \to \alpha {⪯}_{\mathsf{su}}\alpha \}$. If the input is malformed or open, the transducer emits ${\mathcal{I}}_{-}$ and stops.

For each number $i=0,\dots ,N-1$, the record-emission pass rescans the input with a node counter and a prefix-tree depth counter until it reaches node $i$, then emits the clause determined by that constructor. Root and binder variables are the binary node numbers tagged by $a$ or $b$. To find the binder of a variable occurrence, enumerate earlier binder nodes. For each candidate, a rescan computes the interval of node positions occupied by its body and tests whether the occurrence lies in that interval; counting the containing candidates from inside outwards resolves the de Bruijn index. The same enumeration, restricted to lambda candidates, emits the protected sequence from the outermost enclosing lambda to the innermost. Returning from a child requires no stored path: another rescan finds the child’s interval of prefix-tree positions and its parent’s constructor.

Every live value is an input position, node number, depth, binder count, or output-length counter, hence uses $O(\log n)$ bits. There are $O(n)$ constraints and each protected tuple contains at most $n$ tagged variables, so the mixed output has $O(n^2)$ tokens. Converting an equation to the pair inequality of proposition 5.3 adds a fixed wrapper around two copies addressed by rescans and keeps the same polynomial bound. The transducer therefore satisfies definition 5.13. ◻

The converse reduction and the exact negative boundary

The converse construction must preserve one outer substitution while allowing a different matcher for each inequality. A plain lambda binding preserves one type for repeated occurrences and therefore encodes equations. A polymorphic recursive binding permits its occurrences to instantiate the definition type and therefore encodes inequalities. Moving all ordinary bindings under one outer recursive binder leaves only one occurrence of $\mathsf{fix}$; pairing collects the finitely many checks without changing their individual matching substitutions.

It is useful first to separate an auxiliary product calculation from its pure-lambda implementation. In the auxiliary calculation, products have types $\tau \times \rho$, introduction $⟨P,Q⟩:\tau \times \rho$, and the two projections. These are derived bookkeeping rules, not constructors of the target language.

The implementation uses the following pure lambda terms: $$⟨P,Q⟩\equiv \lambda k.kPQ,P.1\equiv P(\lambda u.\lambda v.u),P.2\equiv P(\lambda u.\lambda v.v),$$ with right-nested tuples and their projections defined recursively. Even a one-component tuple is $⟨P,K⟩$ and its component is the first projection; this convention makes the singleton calculation below exercise the same eliminator as a longer family. Write $P{\doteq }_{\lambda }Q$ for $\lambda z.⟨zP,zQ⟩$, and put $K\equiv \lambda u.\lambda v.u$. For the expansion, use the result-indexed abbreviation $$(\tau ,\rho {)}_{\delta }:=(\tau \to \rho \to \delta )\to \delta .$$ Then $⟨P,Q⟩:(\tau ,\rho {)}_{\delta }$ whenever $P:\tau$ and $Q:\rho$. The result type $\delta$ is an index, not a uniquely determined type: the same pair introduction has this type for every $\delta$. A first projection fixes $\delta =\tau$ and a second projection fixes $\delta =\rho$. Applying both projections to one monomorphic pair could therefore force $\tau =\rho$. The encoder below projects each instantiated recursive occurrence once, so every elimination determines only its own result index. The equality gadget is typable exactly when $P$ and $Q$ receive the same monotype.

Rename the arrow constructor of a source problem to the formal product constructor; this signature isomorphism preserves semi-unifiers in both directions. For a vector $\overrightarrow{z}=(z_{\alpha })$ indexed by the source variables, define $⌜M{⌝}_{\overrightarrow{z}}$ by replacing a variable $\alpha$ with $z_{\alpha }$ and a binary node with the auxiliary pair. A simple type environment $A$ on those term variables extends homomorphically through the formal product constructor; write the resulting product type as $A(M)$. In particular, $A(M)$ does not mistake a source binary node for a function type.

Proof of Lemma 5.15 — Representation and substitution correctness

Proof. For item 1, induct on $M$. A variable uses its unique assumption in $A$. At a binary node, the two induction hypotheses and the derived pair rule give the homomorphic pair type; inversion of that rule gives the converse.

For items 2 and 3, the auxiliary signature must first be returned to the one-constructor source signature. Serialize each non-product-rooted auxiliary monotype $T$, and let $\iota (T)$ be the source variable whose index is that serialization. Thus $\iota$ is injective. Define the quotient $q$ by Although $\iota$ is defined on every finite auxiliary monotype, evaluating $q$ on the present finite family queries only finitely many of its values. Define the source substitution $S_A(\alpha )=q(A(\alpha ))$. Structural induction on $M$ gives the commuting equation $$S_A(M)=q(A(M)).$$ If $A(M)=A(N)$, applying $q$ and equation 5.11 shows that $S_A$ unifies $M$ and $N$.

For item 3, let $R_i(A(M_i))=A(N_i)$. A maximal nonproduct component of $A(M_i)$ is a non-product-rooted subtree whose parent, if it has one, is a product. Define a finite source matcher $r_i$ by $$r_i(\iota (T))=q(R_i(T))$$ for every such component $T$, and let $r_i$ fix all other variables. A second structural induction, now on the product skeleton of $A(M_i)$, gives $$r_i(q(A(M_i)))=q(R_i(A(M_i))).$$ Combining the two commuting equations with the witness equality gives the annotated calculation Thus $S_A$ is one shared outer substitution and the $r_i$ are the required source matchers. ◻

Proof of Lemma 5.16 — Result-indexed Church formation and inversion

Proof. Induct on $M$. At a variable leaf, Var gives the type selected by $A$. At a binary node $o$, the induction hypotheses type the two expanded children. Assign $k$ the arrow type ${\mathcal{C}}_{\mathrm{\Delta }}(A,P)\to {\mathcal{C}}_{\mathrm{\Delta }}(A,Q)\to {\delta }_o$; two applications followed by one abstraction give the displayed type.

For inversion, a typing of $\lambda k.kPQ$ ends, after theorem 5.8, with abstraction and two applications. Their arrow equations force types ${\tau }_P,{\tau }_Q,{\delta }_o$ and the result $({\tau }_P\to {\tau }_Q\to {\delta }_o)\to {\delta }_o$. Apply the induction hypotheses to $P$ and $Q$. No rule equates ${\delta }_o$ with another index unless the surrounding term eliminates this occurrence, which is why the assignment is not claimed unique. ◻

For $\mathcal{I}=\{M_i{⪯}_{\mathsf{su}}{N}_i{\}}_{i=1}^m$, let $\overrightarrow{x}$ list its source variables. For each $i$, use a fresh vector ${\overrightarrow{y}}_i$ of the same length. The subscript on $⌜-⌝$ states which vector represents source variables. Define The first argument of $K$ fixes the result type of the recursive definition to the tuple of the $A(M_i)$. The second argument is checked but hidden from that result. The local vector ${\overrightarrow{y}}_i$ supplies an independent instance of the recursive scheme, whereas the right side uses the outer vector $\overrightarrow{x}$. The equality gadget therefore imposes $R_i(A(M_i))=A(N_i)$ rather than comparing two locally instantiated trees.

For the singleton problem $\{\alpha {⪯}_{\mathsf{su}}\beta \to \alpha \}$, the source-variable order $(\alpha ,\beta )$ gives the auxiliary term $$\mathsf{fix}f.\lambda x_{\alpha }{x}_{\beta }.K⟨x_{\alpha },K⟩⟨\lambda y_{\alpha }{y}_{\beta }.((f{y}_{\alpha }{y}_{\beta }).1{\doteq }_{\lambda }⟨x_{\beta },x_{\alpha }⟩),K⟩.$$ Its pure expansion replaces $⟨x_{\alpha },K⟩$ by $\lambda k.k{x}_{\alpha }K$ and $(f{y}_{\alpha }{y}_{\beta }).1$ by $(f{y}_{\alpha }{y}_{\beta })(\lambda u.\lambda v.u)$; expanding the equality gadget gives With outer substitution $S=\mathsf{id}$, the local matcher $R=[\beta \to \alpha /\alpha ]$ types the recursive occurrence at the required component: its projected type becomes $\beta \to \alpha$, the type of the source tree on the right. In the auxiliary calculation, the outer pair $⟨x_{\beta },x_{\alpha }⟩$ has the renamed product type $\beta \times \alpha$. This one inequality exercises the tuple, first projection, equality gadget, $K$, and the independent recursive instance.

Proof of Lemma 5.17 — Whole-encoder Church adequacy

Proof. For the forward construction, process each pair occurrence from its enclosing elimination inward. A first projection assigns its pair index the first component type; an $i$th projection down a right-nested tuple assigns the successive indices to the right-tail types and the final selected index to the $i$th component type. Pair occurrences used only for formation receive fresh indices. The two applications in every projection and the formation calculation of lemma 5.16 then expand the auxiliary derivation. Different recursive occurrences first instantiate the scheme of $f$, so their index assignments are independent.

Conversely, normalize a typing of the pure expansion. Invert each $\lambda k.kPQ$ by lemma 5.16. Invert $P(\lambda u.\lambda v.u)$: the application equation forces the result index of $P$ to equal the first component type. The second projection forces the analogous second-component equation. Replace these introduction and elimination subderivations by the corresponding auxiliary product rules. The equality gadget has body $⟨zP,zQ⟩$; its two applications force $P$ and $Q$ to have the same domain type. The remaining cases are variables, abstraction, application, $K$, and the single fix; their rules are unchanged. Structural induction over the fixed encoder syntax therefore reconstructs the complete auxiliary derivation. ◻

Proof of Theorem 5.18 — Converse reduction

Proof. Work first in the auxiliary product calculation. Suppose that $S$ and $R_i$ semi-unify $\mathcal{I}$. Let $J(T)$ replace every source arrow in $T$ by the auxiliary product. For a source substitution $U$, define the auxiliary substitution $J_{\ast }U$ by $(J_{\ast }U)(\alpha )=J(U(\alpha ))$. Structural induction on $T$ gives $$(J_{\ast }U)(J(T))=J(U(T)).$$ Assign each source term variable $x_{\alpha }$ the type $(J_{\ast }S)(\alpha )$. By lemma 5.15(1), the first tuple in equation 5.13 has component types $J(S(M_i))$. Generalize the type of $f$ at MM-Fix. At its $i$th occurrence, instantiate that scheme with $J_{\ast }{R}_i$; the $i$th projection therefore has type $$(J_{\ast }{R}_i)(J(S(M_i)))=J(R_i(S(M_i)))=J(S(N_i)).$$ The equality gadget, tuple formation, the lambda binders, and $K$ give a typing of the auxiliary term. Apply lemma 5.17 to obtain a pure typing.

Conversely, use lemma 5.17 to reconstruct an auxiliary typing, and normalize it by theorem 5.8. Invert the outer fix, lambdas, and the first tuple. The types of the bound $x_{\alpha }$ determine a simple environment $A$, and lemma 5.15(1) makes the $i$th result component $A(M_i)$. Each recursive occurrence is an independent instance of the generalized type of $f$. Inverting its projection and equality gadget therefore supplies a matcher with $A(M_i){⪯}_{\mathsf{su}}A(N_i)$. Item 3 of the lemma gives one shared outer substitution and one matcher per source inequality. Hence $\mathcal{I}$ is semi-unifiable.

For the space bound, first validate the framed counts and every tree record. Put $$e_{-}:=\mathsf{fix}f.\lambda x.xx,e_{+}:=\mathsf{fix}f.\lambda x.x.$$ A malformed string is sent to the fixed untypable restricted term $e_{-}$. A valid empty family is sent to the fixed typable restricted term $e_{+}$. For a nonempty valid family, use the serializations of definition 5.13. Enumerate distinct source variables by their first input occurrence: for each candidate, rescan the earlier prefix to test whether the same length-delimited name has appeared. To emit the $i$th tuple component or projection, store only the binary counters $i,m$ and rescan to the corresponding inequality. A source tree is emitted by its node number in prefix-tree order; returning from a child is reconstructed by rescanning with node and depth counters, not by storing its path. Right-nested tuples and Church templates add $O(m)$ wrappers, and copied trees give at most quadratic output size. All live counters use $O(\log n)$ bits, so the encoder meets definition 5.13. ◻

Deleting polymorphic recursion collapses the separate occurrences of $f$ to one monotype and destroys equation 5.15.

Proof of Corollary 5.19 — Log-space equivalence

Proof. The first reduction is corollary 5.14. The second is theorem 5.18. For the remaining reduction, parse the input as the item-3 fragment. A well-formed fragment term is copied unchanged. A malformed string or a well-formed term outside the fragment is sent to the fixed untypable unrestricted term $u_{-}:=\lambda x.xx$. The parser uses counters for framing, binder depth, and the number and position of $\mathsf{fix}$ tokens, hence logarithmic work space. This guarded copy preserves both positive and negative instances on the whole string language. ◻

The source of undecidability can be stated at an even smaller signature.

Proof of Lemma 5.21 — The one-tape source is r.e.-complete

Proof. A one-tape universal simulator recognizes ${\mathsf{HaltTM}}_1$: it stores the simulated finite nonblank tape interval with a marked head, scans to the encoded transition table, rewrites the marked cell, and repeats. It halts exactly when the simulated machine halts, so the source is recursively enumerable.

Let $P$ be recursively enumerable, witnessed by a fixed one-tape machine $T_P$. The function $w\mapsto \mathsf{join}(\mathsf{code}(T_P),w)$ is total computable and its output belongs to ${\mathsf{HaltTM}}_1$ exactly when $w\in P$. Hence every recursively enumerable language reduces to the source. ◻

Proof of Lemma 5.22 — The one-tape source is undecidable

Proof. Suppose a total machine $H$ returned yes exactly on the halting pairs. Build a one-tape machine $D$ which, on input $x$, runs $H$ on the framed pair $\mathsf{join}(x,x)$, loops when $H$ returns $1$, and halts when $H$ returns $0$. The finite transition table of $D$ has the structural serialization $d=\mathsf{code}(D)$. On input $d$, $$D(d)\text{ halts}⟺H(\mathsf{join}(d,d))\text{ returns }0⟺D(d)\text{ does not halt},$$ a contradiction. ◻

Proof of Lemma 5.23 — Finite support for semi-unification

Proof. Every replay inspects the outer valuation only at variables in the input trees. Its matched left side then inspects $R_i$ only at variable leaves of $S(M_i)$. Restricting the valuations to those finite domains therefore preserves every replay equation. Conversely, extend each finite map by the identity on variables outside its domain. Homomorphic extension on the finite input trees gives the same replay, so the extensions are total solutions. ◻

Dudenhefner’s one-tape library model packages a finite state type, a total transition on a state and one optional tape symbol, a Boolean halting test, and an initial tape. The value $\mathsf{None}$ denotes a blank cell and $\mathsf{Some}(a)$ denotes a cell containing $a$; the move component is left, right, or stationary. Write ${\mathsf{HaltTM}}_1^{\mathrm{lib}}$ for its halting language.

Proof of Lemma 5.24 — Machine-model bridge

Proof. Use the local tape alphabet as the library alphabet and represent a blank cell by $\mathsf{None}$ and a written symbol by $\mathsf{Some}(a)$. The library state type is the finite local state set plus one fresh sink. On a defined local transition, $\hat{T}$ writes the corresponding optional symbol, moves left or right, and enters the corresponding state. On an undefined nonhalting transition, it enters the sink; the sink writes the same symbol, does not move, and loops. The library Boolean halting test is true exactly at the image of the designated local halting state. Place the letters of $w$ in consecutive optional cells to obtain $t_w$.

Let ${\iota }_Q$ be the inclusion of the local state set into the enlarged library state set. For a local configuration $c=(q,h,t)$, define For every defined nonhalting local step $c{⟶}_T{c}^{\prime }$, direct inspection of the transition table gives $E(c){⟶}_{\hat{T}}E(c^{\prime })$. Induction on the number of local steps gives the forward simulation. Conversely, a library run that reaches a Boolean-halting state never entered the sink, so inversion of each preceding transition reconstructs the local run. The construction traverses finite transition tables, state lists, and the word $w$, so a one-tape transducer computes its framed serialization by repeated scans and copying. ◻

Proof of Theorem 5.25 — Exact constructive reduction import

Proof. The imported theorem has the library source ${\mathsf{HaltTM}}_1^{\mathrm{lib}}$, not the local partial-transition source. Dudenhefner’s Theorem 5.23 and its mechanized Section 6 endpoint prove ${\mathsf{HaltTM}}_1^{\mathrm{lib}}{▹}_{\mathsf{m}}\mathsf{SemiU}$ [Dud23]. The imported construction is the composition through binary Post correspondence, binary stack-machine halting, two-counter halting, one-counter halting, deterministic and confluent stack-machine uniform boundedness, simple semi-unification, and right-uniform two-inequality semi-unification. The source proves every component reduction and their composition; reconstructing that development would require more than ten pages. The paper’s variables are natural numbers, its terms are generated only by variables and one binary arrow, and its solutions are total valuations.

Let $G$ denote the imported Coq reducer. It is a terminating structural program on finite inductive encodings. A one-tape evaluator stores the current framed constructor record beside an explicit stack of pending subterms, scans the finite program table to select the next clause, and writes the resulting framed constructor record at the right end of its work tape. Induction on the finite recursive call tree shows that, on input $x$, this evaluator writes the structural serialization of $G(x)$. Termination of $G(x)$ therefore gives termination of the evaluator. The input and output serializers consequently realize a total computable string function.

Compose that function with lemma 5.24. A malformed local source string is sent to the named negative problem ${\mathcal{I}}_{-}$ from the forward reduction. Lemma 5.23 supplies exactly the finite-substitution consequence used in this chapter. ◻

Proof of Theorem 5.26 — Constructive semi-unification boundary

Proof. By lemma 5.21, theorem 5.25, semi-unification is r.e.-hard.

For recursive enumerability, code variables as ${\alpha }_0,{\alpha }_1,\dots$. At stage $n$, enumerate every outer substitution on $\mathrm{ftv}(\mathcal{I})$ whose range trees have total size at most $n$ and use only ${\alpha }_0,\dots ,{\alpha }_n$. For each candidate $S$ and each inequality $M_i{⪯}_{\mathsf{su}}{N}_i$, compute the finite domain $D_i=\mathrm{ftv}(S(M_i))$; enumerate all matchers on $D_i$ with the same size and variable bound. Test the equations and all structural replays. Every loop at stage $n$ is finite. Every finite witness is alpha-renamable into some stage, and lemma 5.23 shows that no total valuation witness is missed. Dovetailing the stages therefore halts exactly on the semi-unifiable inputs. Thus the problem is recursively enumerable as well as r.e.-hard. ◻

Proof of Corollary 5.27 — Undecidability

Proof. If the restricted typability problem were decidable, compose its decider with theorem 5.18. This would decide the recursively enumerable complete problem of theorem 5.26, contradicting lemma 5.22. ◻

For example, the annotation $\mathrm{\forall }\alpha .\alpha \to \alpha$ accepts the body $\lambda x.x$: replacing $\alpha$ by $\kappa$ gives target $\kappa \to \kappa$, so the lambda binds $x:\kappa$ and its variable body checks at $\kappa$. The annotation $\mathrm{\forall }\alpha .\alpha$ rejects the same body. The lambda would require the equation $\kappa =\beta \to \beta$ for a flexible $\beta$, but solving it would replace the rigid constant $\kappa$.

Bibliographic notes.

The Milner–Mycroft calculus, syntax-directed normalization, and the two reduction architectures originate in Henglein’s development [Hen93]; the recursive typing discipline was introduced by Mycroft [Myc84]. The constructive arrow-only boundary and exact import used here are due to Dudenhefner [Dud23]; the earlier proof route and a compact mechanized middle reduction are recorded in [Dud20].