跳轉到

1937 - Post 的字元產生系統（Post Canonical System）#

案件摘要#

1937 年，Emil Post 走上一條與 Church、Turing 完全獨立的路線，用「符號字串的重寫與產生」刻畫可計算性。本案追查：一條條簡單的 \(u \to v\) 產生規則，如何重寫出整個計算宇宙。

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

  • 1920 年代，Post 在普林斯頓（師從 Veblen）研究 Whitehead–Russell《數學原理》的命題演算，試圖找出完備的決策程序。
  • 1921 年前後他發現命題演算「不可窮盡」——事實上他預見了不可判定性，但因病與種種因素延遲發表。
  • 轉向更根本的問題：什麼樣的符號操作過程是「機械的」？ 他稱之為「1- generability」。

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

1. 產生規則的形式#

Post 正則系統由有限組產生規則（production）構成，每條規則形如：

\[ \frac{g_1 u_1 \, g_2 u_2 \, \cdots \, g_n u_n \, g_{n+1}}{h_1 v_1 \, h_2 v_2 \, \cdots \, h_m v_m \, h_{m+1}} \]

其中 \(g_i, h_j\) 是固定字串（常數）， \(u_i, v_j\) 是變元（variables），且每個變元 \(v_j\) 必須是某些 \(u_i\) 的複製。意思是：若公理集產生的字串能匹配前提模式（ \(g_i\) 之間插入任意 \(u_i\) ），就能產生結論模式。

最簡版本（正規規則）：

\[ u \;\to\; v \quad (\text{若字串 } gu \text{ 可導出，則 } hv \text{ 亦可導出}) \]

2. Python 模擬：Tag 系統式的字串改寫#

Post 的著名特例是 tag 系統：刪去字串開頭 \(p\) 個符號，依刪去的首符號在字尾附加固定字串。

# Post 的 tag 系統 (p=2)：讀首符號，刪兩個，尾附加對應字串
rules = {'a': 'aa', 'b': 'aaaa'}   # 對應 μ 倍增，模擬簡單運算

def tag(s, max_steps=20):
    for i in range(max_steps):
        print(i, s)
        if len(s) < 2:
            return s
        s = s[2:] + rules[s[0]]
    return None

tag('aab')
# 0 aab
# 1 b aa          -> aaaa
# 2 aa aaaa       -> ...

# 一般化 Post 正則系統：匹配 -> 產生
def post_derive(axioms, rules, max_words=50):
    words, seen, i = set(axioms), set(axioms), 0
    while i < max_words:
        new = set()
        for w in words:
            for lhs, rhs in rules:          # lhs 含變元 A,B
                for k in range(1, len(w)):
                    if w.startswith(lhs.replace('A', '')):
                        v = w[len(lhs)-1:]   # 取出變元部分
                        new.add(rhs.replace('A', v))
        words |= new - seen
        seen |= new
        i += 1
    return sorted(seen)

# 規則：xA -> Axx (產生 xx^n) 模擬「複製」能力
print(post_derive(['ab'], [('a', 'aa')]))

3. 等價性：Post 系統 ≡ 圖靈機 ≡ λ 演算#

Post 證明（並於 1943、1947 論文補全）： - (Post ⊇ Turing) 圖靈機的瞬時組態（紙帶內容 + 磁頭位置 + 狀態）可編碼為一個字串；機器的每一步移動對應一條有限組產生規則。於是「機器的所有可能計算史」恰為系統可產生的字串集。 - (Turing ⊇ Post) 任何正則系統的推導可用圖靈機模擬：機器維護目前字串，逐一嘗試規則匹配。 - Post 也證明其系統與 λ 可定義函數等價。

因此 Post 稱他的系統刻畫了「所有機械式組合過程」——這是 Church–Turing 命題的第三條獨立證據。

4. 對 Chomsky 文法與形式語言的影響#

Post 系統是所有字元重寫系統的祖宗： | 系統 | 規則形式 | 限制 | |---|---|---| | Post 正則系統 | \(\frac{\text{模式}}{\text{模式}}\) （變元可複製） | 最一般 | | 無限制文法（Type 0） | \(\alpha \to \beta\) | 左右皆可為字串 | | 單向文法（Type 1） | \(\alpha A \beta \to \alpha \gamma \beta\) | 不縮短 | | CFG（Type 2） | \(A \to \gamma\) | 左端單一非終端 | | 正則文法（Type 3） | \(A \to aB\) 或 \(A \to a\) | 最受限 |

Chomsky (1956, 1959) 的文法階層本質上是 Post 系統的約束版本；L-systems（Lindenmayer, 1968）、Thue 系統、Markov 演算法皆是同一家族。

結案 -- 後果與影響#

  • 確立「符號重寫」作為計算的第三種範式（繼 λ 演算、圖靈機之後），三者後來成為函數式、命令式、產生式三大計算模型的源頭。
  • Post 系統直接催生形式語言理論與 Chomsky 階層，影響編譯器、正則表示式、程式語言設計。
  • Post 1947 年證明 Thue 系統的字問題不可判定，是第一個「代數問題不可判定」的例子。

關鍵人物與文獻#

  • Emil Post（1897–1954），生於波蘭華沙（當時屬俄國），幼年移民紐約，任職紐約市立學院；曾於普林斯頓深造。
  • Post, E. (1936/1943). "Finite combinatory processes - formulation 1." J. Symbolic Logic 1:103–105；"Formal reductions of the general combinatorial decision problem." Amer. J. Math. 65:197–215.
  • Post, E. (1947). "Recursive unsolvability of a problem of Thue." J. Symbolic Logic 12:1–11.
  • 相關：Chomsky (1956)、Davis, Computability and Unsolvability (1958)。