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

DOI10.46298/LMCS-19(4:22)2023MaRDI QIDQ6137845zbMATH OpenFDO

Authors Andrej Dudenhefner

Publication date 16 January 2024

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2208.13428

zbMATH Keywords

constructive mathematicsundecidabilitycomputability theoryCoqsemi-unificationmechanization

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

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.

Recommendations

• Constructive many-one reduction from the halting problem to semi-unification
• The undecidability of the semi-unification problem
• scientific article; zbMATH DE number 2085172
• Semi-unification
• scientific article; zbMATH DE number 4092757

Cites work

• scientific article; zbMATH DE number 3874579 (Why is no real title available?)
• scientific article; zbMATH DE number 4035120 (Why is no real title available?)
• scientific article; zbMATH DE number 4092757 (Why is no real title available?)
• scientific article; zbMATH DE number 125891 (Why is no real title available?)
• scientific article; zbMATH DE number 176152 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 1354168 (Why is no real title available?)
• scientific article; zbMATH DE number 7566048 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus
• A formalization of multi-tape Turing machines
• A theory of type polymorphism in programming
• A variant of a recursively unsolvable problem
• An analysis of ML typability
• Constructive many-one reduction from the halting problem to semi-unification
• Counter machines
• First steps in synthetic computability theory
• On Forward Closure and the Finite Variant Property
• On immortal configurations in Turing machines
• Periodicity and Immortality in Reversible Computing
• Small universal register machines
• The Tiling Problem Revisited (Extended Abstract)
• The surveyability of mathematical proof: A historical perspective
• The undecidability of the Turing machine immortality problem
• The undecidability of the semi-unification problem
• Typability and type checking in System F are equivalent and undecidable
• Unification modulo synchronous distributivity
• Verification of PCP-related computational reductions in Coq

Cited in

(1)

• Constructive many-one reduction from the halting problem to semi-unification

This page was built for publication: Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6137845)