一句话：给出停机问题到半合一的构造性多一归约，并用无公理 Coq 机械化证明其 RE 完全性。
半合一是 first-order unification 与 first-order matching 的组合。Kfoury、Tiuryn 和 Urzyczyn 在 1990 年代通过从图灵机不朽性（存在发散配置）出发的 Turing 归约证明了其不可判定性，但该归约复杂、依赖非构造性原则并涉及多种中间计算模型。本文给出从图灵机停机问题到半合一的构造性多一归约，从而在 many-one 归约下建立半合一的 RE 完全性。作者在 Coq 证明助手中给出无公理机械化，见证归约函数的可计算性、论证的构造性与正确性，并将其并入现有的 Coq 不可判定性证明库；机械化还包含 Hooper 不朽性论证的一个变体。
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.
@article{paperbot2173,
title = {Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)},
author = {Andrej Dudenhefner},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:22)2023}
}