Semi-unification and Milner–Mycroft inference

First-order terms use variables and one binary arrow constructor. A semi-unification witness has one finite outer substitution and one finite matcher per inequality. The pure term calculus has variable, abstraction, application, nonrecursive let, and polymorphic $\mathsf{fix}$; schemes are predicative quantifier prefixes over arrow monotypes.

Equation encoding, the finite-tree obstruction, syntax-directed normalization, mutual-protected-renaming, scheme representation, and the generated-constraint characterization are proved in chapter 5. The characterization keeps one outer substitution through every constructor and yields a log-space reduction from closed Milner–Mycroft typability to semi-unifiability. The converse section separates abstract products, indexed Church formation/inversion, and the whole-encoder retraction before constructing its one-fix encoder.

The converse log-space encoder, its representation, indexed Church adequacy, and both correctness directions are derived locally for finite binary problems. The encoder yields a pure term with one top-level $\mathsf{fix}$, no inner $\mathsf{fix}$, and no $\mathsf{let}$. The exact imported result is Dudenhefner’s Theorem 5.23, from the library’s total-transition machine and initial-tape model to total-valuation arrow-only semi-unification. Lemma 5.24 translates the chapter’s partial-transition word-input machines to that source. Lemma 5.23 and fair enumeration then transfer the target signature to finite substitutions and prove recursive enumerability.

Undecidability concerns existence of a typing for an unannotated term. It does not apply to ordinary HM, to checking a supplied finite derivation, or to checking a fixed polymorphic-recursion annotation.

The Kappa companion in artifacts/ch5-semi-unification-reduction/ implements finite substitutions, equation replay, one matcher per inequality, and the displayed node-count rejection certificate. It proves none of the reductions or undecidability results.