Edith Heiter: Bachelor's Thesis

Saarland University Computer Science

Undecidability of the Post Correspondence Problem in Coq

Advisors: Yannick Forster, Gert Smolka

Abstract

We study, formalize, and verify reductions of the halting problem for Turing machines (Halt) to the Post correspondence problem (PCP). The formalizations and verifications are carried out with the interactive theorem prover Coq with constructive proofs not using excluded middle. We verify 7 reductions: Halt to SR (word problem for string rewriting), SR to MPCP (Post correspondence problem with fixed first domino) and MPCP to PCP. We present an alternative, direct reduction of Halt to MPCP, and reductions of SR to RSR (word problem for string rewriting with nonempty rules) as well as RSR to PCP. In addition, the reduction of Halt to SR includes a reduction of the reachability problem for Turing machines (Reach) to SR. We observe that the correctness of the reductions is argued rather informally in the literature and that the formal verification requires considerable elaboration and effort.

References

Thesis and Formalization

Presentations


Edith Heiter, Thu Aug 24 13:46:54 2017