Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Andrej Dudenhefner

TL;DR

The work presents a constructive, axiom-free chain of many-one reductions from the Turing machine halting problem to semi-unification, establishing $R E$-completeness under many-one reductions. It replaces reliance on Turing machine immortality with a uniform boundedness approach via one-counter and two-stack machines, and ultimately to a fragment of semi-unification, all mechanized in Coq and integrated into the CLUP20 library. The reductions are carefully modular, with each step proven constructively and mechanically, ensuring global and local surveyability of the argument. The mechanization not only certifies correctness but also demonstrates a practical pathway to mechanize related undecidability results, such as System F typability, and paves the way for further formalized reductions in computability theory.

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.

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

TL;DR

The work presents a constructive, axiom-free chain of many-one reductions from the Turing machine halting problem to semi-unification, establishing -completeness under many-one reductions. It replaces reliance on Turing machine immortality with a uniform boundedness approach via one-counter and two-stack machines, and ultimately to a fragment of semi-unification, all mechanized in Coq and integrated into the CLUP20 library. The reductions are carefully modular, with each step proven constructively and mechanically, ensuring global and local surveyability of the argument. The mechanization not only certifies correctness but also demonstrates a practical pathway to mechanize related undecidability results, such as System F typability, and paves the way for further formalized reductions in computability theory.

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.
Paper Structure (15 sections, 19 theorems, 13 equations)

This paper contains 15 sections, 19 theorems, 13 equations.

Table of Contents

  1. Introduction
  2. Two-counter Machines
  3. One-counter Machines
  4. Two-stack Machines
  5. Deterministic, Length-preserving Two-stack Machines
  6. Confluent, Simple Two-stack Machines
  7. Semi-unification
  8. Simple Semi-unification
  9. Right/Left-Uniform, Two-inequality Semi-unification
  10. Main Result
  11. Mechanization
  12. One-counter Machines
  13. Deterministic, Length-preserving Two-stack Machines
  14. Confluent Two-stack Machines
  15. Conclusion

Key Result

Lemma 2.4

The Turing machine halting problem many-one reduces to the two-counter machine halting problem (Problem prb:cm2halt).

Theorems & Definitions (74)

  • Definition 2.1: Two-counter Machine ($\mathcal{M}$)
  • Remark 2.2
  • Lemma 2.4
  • proof : Proof Sketch
  • Corollary 2.5
  • Remark 2.6
  • Remark 2.7
  • Example 2.8
  • Definition 3.1: One-counter Machine ($\mathcal{P}$)
  • Example 3.2
  • ...and 64 more