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在1990年代通过从图灵机永存性（存在发散配置）的图灵归约证明了半合一问题的不可判定性。该特定的图灵归约过程复杂，使用了非计算原理，并涉及多种中间计算模型。本文给出了从图灵机停机问题到半合一问题的构造性多一归约，从而确立了半合一问题在多一归约下的RE完备性。归约函数的可计算性、论证的构造性以及正确性均通过Coq证明助手中的无公理机械化实现得到验证。这为该结果提供了全面、精确且可检验的证据。该机械化实现已被纳入现有的、维护良好的Coq不可判定性证明库中。值得注意的是，Hooper关于图灵机永存性不可判定性的论证变体是此机械化实现的一部分。