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

DOI10.46298/LMCS-19(4:22)2023arXiv2208.13428MaRDI QIDQ6137845FDOQ6137845

Andrej Dudenhefner

Publication date: 16 January 2024

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

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.

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)

Cites Work

• A theory of type polymorphism in programming
• Title not available (Why is that?)
• Small universal register machines
• Title not available (Why is that?)
• The undecidability of the semi-unification problem
• Typability and type checking in System F are equivalent and undecidable
• A variant of a recursively unsolvable problem
• A formalization of multi-tape Turing machines
• Title not available (Why is that?)
• Periodicity and Immortality in Reversible Computing
• The undecidability of the Turing machine immortality problem
• The Tiling Problem Revisited (Extended Abstract)
• First steps in synthetic computability theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• An analysis of ML typability
• Title not available (Why is that?)
• On Forward Closure and the Finite Variant Property
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Counter machines
• Verification of PCP-related computational reductions in Coq
• On Immortal Configurations in Turing Machines
• A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus
• The surveyability of mathematical proof: A historical perspective
• Unification Modulo Synchronous Distributivity
• Title not available (Why is that?)
• Title not available (Why is that?)

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)