The halting problem reduces to Post's correspondence problem

DescriptiveComplexity.halt_ordered_fo_reduction_pcp: the classical computation-history dominoes, as an ordered first-order reduction HALT ≤ᶠᵒ[≤] PCP. The machine of the instance is data, so the reduction writes one rule domino per combination of transition attributes, the copy and bookkeeping dominoes beside them, and the initial configuration – the input page between two endmarkers, with a boot letter in the state slot – as the one long word of the start domino.

The construction is layered below this file:

• Problems/Pcp/Hardness/History.lean – dominoes decide derivability, for any string-rewriting system with nonempty rule sides;
• Problems/Pcp/Hardness/ConfigWord.lean – the rewriting system of a machine on the unbounded tape: derivability of the halting word is acceptance;
• Problems/Pcp/Hardness/Draw.lean – the elements and word tables of the drawn PCP instance;
• Problems/Pcp/Hardness/Match.lean – an instance reading as the drawing has a match exactly when the machine accepts;
• Problems/Pcp/Hardness/Interp.lean – the defining formulas realize the drawing.

With DescriptiveComplexity.pcp_mem_RE this makes PCP RE-complete as soon as HALT is RE-hard, which is DescriptiveComplexity.halt_RE_hard (DescriptiveComplexity.Problems.Machine.HaltHard).

noncomputable def DescriptiveComplexity.halt_ordered_fo_reduction_pcp : OrderedFOReduction HALT PCP

HALT ≤ᶠᵒ[≤] PCP: the computation-history dominoes of the machine described by the instance.

Equations

• One or more equations did not get rendered due to their size.