1943 - Post 對應問題（Post Correspondence Problem, PCP）#

案件摘要#

1943 年，Emil Post 提出一個看起來像拼圖遊戲的問題：給定一組上下兩列字串的「磚塊」，能否排出一列使上下字串相同？這個天真簡單的問題竟是不可判定的。本案追查 PCP 如何成為不可判定性證明的「標準跳板」。

前因 -- 為什麼會有這個案子#

Post 在 1937 年的正則系統研究中，把一般組合決策問題歸約到字串操作層面，需要一個「最小而不可判定」的字串問題作為基準。
1947 年他證明 Thue 系統字問題不可判定；PCP（1946 提出，1943 年代論文中成形）則是更精簡的跳板。
動機：許多形式語言/文法問題（如 CFG 的等價性、交集非空性）很難直接歸約自停機問題，但很容易歸約自 PCP。

線索與推理 -- 數學式、程式、理論#

1. PCP 問題定義#

給定有限組「磚塊（tiles/dominoes）」，每塊有上列 \(b_i\) 與下列 \(t_i\) ：

\[ \left[\frac{b_1}{t_1}\right],\ \left[\frac{b_2}{t_2}\right],\ \dots,\ \left[\frac{b_k}{t_k}\right], \quad b_i, t_i \in \Sigma^+ \]

問題：是否存在索引序列 \(i_1, i_2, \dots, i_m\) （ \(m \ge 1\) ，可重複使用磚塊）使得：

\[ b_{i_1} b_{i_2} \cdots b_{i_m} \;=\; t_{i_1} t_{i_2} \cdots t_{i_m} \]

2. 範例#

磚塊： \(\left[\frac{ab}{a}\right],\ \left[\frac{b}{abb}\right]\) ？無解。而：

\[ \left[\frac{1}{111}\right],\ \left[\frac{10111}{10}\right] \]

有解：取序列 \((2,1,1,2)\) ：

\[ \underbrace{10111}_{2}\,\underbrace{1}_{1}\,\underbrace{1}_{1}\,\underbrace{10111}_{2} = 101111110111 = \underbrace{10}_{2}\,\underbrace{111}_{1}\,\underbrace{111}_{1}\,\underbrace{10}_{2} \]

3. 不可判定性證明概述（歸約自圖靈機）#

標準歸約（Komin 1972 / Hopcroft–Ullman 教科書版本）： 1. 給定圖靈機 \(M\) 與輸入 \(w\) ，構造一組 PCP 磚塊使得：

\[ M \text{ 停機於 } w \iff \text{對應 PCP 有解} \]

磚塊編碼計算的瞬時組態（紙帶內容 + 磁頭 + 狀態），分四類：
起始磚： \(\left[\frac{\#}{\# \, q_0 w \, \#}\right]\) （上列落後，下逼迫模擬第一步）
模擬磚：對每個轉移 \(\delta(q, a) = (q', b, R)\) ，磚 \(\left[\frac{a}{b}\right]\) 並配狀態傳遞磚 \(\left[\frac{q a}{b q'}\right]\) （右移）；左移類似。
複製磚： \(\left[\frac{a}{a}\right]\) （維持紙帶其他格不變）。
結尾磚： \(\left[\frac{\#}{\#}\right]\) 與停機時的收尾磚，用補字元 \(*\) 處理長度增長。
關鍵不變量：任何部分匹配中，下側總是「上側再多模擬一步」的組態。唯有當 \(M\) 真的停機時，才能用結尾磚把兩列追平——匹配完成即停機。
故若 PCP 可判定，則停機問題可判定，矛盾。 \(\therefore\) PCP 不可判定。
甚至限制 \(\Sigma = \{a, b\}\) 、磚數 \(\ge 5\) （後改良至更少）仍不可判定（Neary 2015 證明 \(n=5\) 不可判定）。

4. PCP 作為標準「跳板」：歸約鏈#

\[ \text{停機問題} \;\le_m\; \text{PCP} \;\le_m\; \left\{ \begin{array}{l} \text{CFG 交集是否非空} \\ \text{CFG 是否有歧義} \\ \text{兩個 CFG 是否等價（的否定方向）} \\ \text{邏輯程式/字串重寫系統的終止性} \\ \text{矩陣半群問題（如 } S \ni \begin{pmatrix} 0&0\\0&0\end{pmatrix}\text{？）} \end{array} \right. \]

證明新問題不可判定的標準套路：構造一組磚塊，把 PCP 的解編碼成該問題的解。

5. Python：回溯搜尋求解小規模 PCP#

PCP 不可判定 ⇒ 沒有萬能演算法，但小實例可用回溯 + 剪枝（前綴/長度檢查）搜尋：

def solve_pcp(tiles, max_depth=12):
    """tiles: [(top, bottom), ...]；回溯搜尋解序列"""
    sols = []

    def extend(seq, top, bot):
        if top == bot and seq:                 # 上下列相等且非空 -> 找到解
            sols.append(list(seq)); return
        if len(seq) >= max_depth:
            return
        for i, (b, t) in enumerate(tiles):
            nb, nt = top + b, bot + t
            # 剪枝 1：誰都不是誰的前綴 -> 永遠追不平
            if not (nt.startswith(nb) or nb.startswith(nt)):
                continue
            # 剪枝 2：長度差距不可能靠剩餘磚塊追平（最短磚長下界）
            if abs(len(nb) - len(nt)) > max_depth * max(len(x) for x in tiles[0]):
                continue
            seq.append(i)
            extend(seq, nb, nt)
            seq.pop()

    extend([], '', '')
    return sols

tiles = [('10111', '10'), ('1', '111'), ('10', '10111')]
# 與文中範例對應，磚塊順序不同但等價
print(solve_pcp(tiles, max_depth=8))
# 例如輸出: [[0, 1, 1, 2]]  -> 10111 1 1 10 == 10 111 111 0... 
# （驗證上下兩列皆為 101111110111 / 101111110111 的對應磚序）

# 驗證
seq = solve_pcp(tiles, max_depth=8)[0]
top = ''.join(tiles[i][0] for i in seq)
bot = ''.join(tiles[i][1] for i in seq)
print(top, bot, top == bot)   # True

結案 -- 後果與影響#

PCP 成為形式語言理論中最常用的不可判定性來源：CFG 歧義性、文法等價性、重寫系統終止性等結果幾乎都經由 PCP 歸約。
展示了不可判定性可以藏身於「看似純組合、與計算無關」的簡單問題中，深刻影響了對「演算法極限」的直覺。
在實務上催生了終止性分析工具（如重寫系統、邏輯程式的驗證器）以 PCP 變體為理論界線。

關鍵人物與文獻#

Emil Post（1897–1954），紐約市立學院。
Post, E. (1946). "A variant of a recursively unsolvable problem." Bull. Amer. Math. Soc. 52:264–268.
Hopcroft, J. & Ullman, J. (1979). Introduction to Automata Theory, Languages, and Computation, §8.5（標準歸約）.
Neary, R. (2015). "Undecidability in binary tag systems and the Post correspondence problem for five pairs of tiles." STACS 2015.
相關：Post (1947, Thue 系統)、Minsky (1967)。