Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)

TL;DR

This paper presents a constructive many-one reduction from the halting problem to semi-unification, proving RE-completeness and mechanizing the proof in Coq for clarity and rigor.

Contribution

It provides the first constructive many-one reduction from the halting problem to semi-unification, with a mechanized, axiom-free proof in Coq.

Findings

Establishes RE-completeness of semi-unification

Mechanized proof in Coq confirms correctness and constructivity

Incorporates variant of Hooper's argument for undecidability

Abstract

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.