Verification of PCP-Related Computational Reductions in Coq

TL;DR

This paper formally verifies multiple computational reductions related to the Post correspondence problem (PCP) using Coq, filling gaps in the literature with rigorous correctness proofs for these reductions.

Contribution

It provides the first formal verification of several PCP-related reductions in Coq, including those to string rewriting, intersection, and palindrome problems.

Findings

Verified reductions from string rewriting to PCP

Verified reductions from PCP to intersection and palindrome problems

Filled gaps in literature with rigorous correctness proofs

Abstract

We formally verify several computational reductions concerning the Post correspondence problem (PCP) using the proof assistant Coq. Our verifications include a reduction of a string rewriting problem generalising the halting problem for Turing machines to PCP, and reductions of PCP to the intersection problem and the palindrome problem for context-free grammars. Interestingly, rigorous correctness proofs for some of the reductions are missing in the literature.