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