Semi-unification is the combination of first-order unification and first-order matching. The undecidability of semi-unification has been proven by Kfoury, Tiuryn, and Urzyczyn in the 1990s by Turing reduction from Turing machine immortality (existence of a diverging configuration). The particular Turing reduction is intricate, uses non-computational principles, and involves various intermediate models of computation. The present work gives a constructive many-one reduction from the Turing machine halting problem to semi-unification. This establishes RE-completeness of semi-unification under many-one reductions. Computability of the reduction function, constructivity of the argument, and correctness of the argument is witnessed by an axiom-free mechanization in the Coq proof assistant. Arguably, this serves as comprehensive, precise, and surveyable evidence for the result at hand. The mechanization is incorporated into the existing, well-maintained Coq library of undecidability proofs. Notably, a variant of Hooper's argument for the undecidability of Turing machine immortality is part of the mechanization.

翻译：半合一是将一阶合一与一阶匹配相结合的问题。Kfoury、Tiuryn和Urzyczyn在20世纪90年代通过从图灵机不死性（存在发散配置）的图灵归约证明了半合一问题的不可判定性。该特定的图灵归约方法复杂，运用了非计算性原理，并涉及多种中间计算模型。本文给出了从图灵机停机问题到半合一问题的构造性多一归约，从而确立了半合一问题在多一归约下的RE完备性。归约函数的可计算性、论证的构造性以及正确性通过Coq证明助手中的无公理机械化实现得到验证。这为该结果提供了全面、精确且可查验的证据。该机械化实现已整合至现有的、维护良好的不可判定性证明Coq库中。值得注意的是，Hooper关于图灵机不死性不可判定性论证的一个变体也包含在此机械化实现中。