形式陈述

Post 对应问题的实例是有限多张牌

$$ \left(\frac{u_1}{v_1},\ldots,\frac{u_k}{v_k}\right), \qquad u_i,v_i\in\Sigma^+. $$$$(\frac{u_1}{v_1},\dots ,\frac{u_k}{v_k}),u_i,v_i\in {\mathrm{\Sigma }}^{+}.$$

问题询问是否存在长度 $m\ge1$$m\ge 1$ 的指标序列 $i_1,\ldots,i_m$$i_1,\dots ,i_m$（允许重复），使

$$ u_{i_1}\cdots u_{i_m}=v_{i_1}\cdots v_{i_m}. $$$$u_{i_1}\cdots u_{i_m}=v_{i_1}\cdots v_{i_m}.$$

在含至少两个符号的字母表上，该判定问题不可判定；常见证明从图灵机接受计算或修改版 PCP 作映射归约。要求非空序列，否则空连接会让所有实例平凡成立。

直觉

每次选择同一张牌，必须同时给上下两行追加不同字符串；局部选择能否在某个未知长度上使两条全局拼接完全同步，足以编码任意计算历史。

例子与边界

牌 $(a/ab),(ba/a)$$(a/ab),(ba/a)$ 选择序列 $1,2$$1,2$ 时，上串为 $aba$$aba$、下串也为 $aba$$aba$，所以有解。搜索所有有限序列可半判定“有解”，但无解时可能永远搜索。不同教材允许空字符串或规定首牌的变体；这些版本之间需显式归约，不能在不改证明时混用。

推论与应用

PCP 是证明文法歧义、CFG 交非空、矩阵与字符串系统不可判定性的通用中介。它展示一个只有有限牌和字符串连接的朴素问题也能承载通用计算。

参考资料

• Michael Sipser, Introduction to the Theory of Computation, 3rd ed., Cengage, 2013，Ch. 5, Post correspondence problem and undecidability reductions。
• Hartley Rogers Jr., Theory of Recursive Functions and Effective Computability, MIT Press, 1987，Chs. 12–13, correspondence systems and recursively enumerable sets。