1973 年 Boyer-Moore 證明器：歸納法的自動偵探#

報案人：Robert Boyer 與 J Strother Moore（愛丁堡大學，後赴德州）。涉案物：一台只懂 Lisp 卻會做數學歸納法的機器。代號：Nqthm。

案發現場#

1970 年代初，自動定理證明的主流是歸結原理。它擅長一階邏輯的短證明，卻在一個地方屢屢失手：數學歸納法。要證「 \(append\) 滿足結合律」「 \(reverse\) 對合」這類程式性質，歸結器只能盲目展開公理，找不到歸納假設藏在哪裡。

另一邊，Lisp 程式滿天飛，卻沒人能保證它們正確。 Boyer 與 Moore 在愛丁堡目睹了這個裂縫：程式用遞迴定義，性質用歸納證明，兩者明明是同一枚硬幣，機器卻看不出來。

1973 年，兩人立志打造一台「懂歸納」的證明器：輸入 Lisp 函數定義與猜想，機器自動選歸納變元、丟出引理、完成證明。這就是 Boyer-Moore 證明器，後來的 Nqthm 與 ACL2 的前身。

偵探的第一個發現：遞迴定義本身就藏著歸納模式。例如自然數與串列：

\[ nat ::= 0 \mid s(n) \]

\[ list ::= nil \mid cons(x, xs) \]

Lisp 的 \(append\) 定義為：

\[ append(nil, y) = y \]

\[ append(cons(a, x), y) = cons(a, append(x, y)) \]

要證性質 \(P(x)\) 對一切 \(x\) 成立，只需證 \(P(nil)\) 與 \(P(x) \to P(cons(a, x))\) 。一般模式為：

\[ \frac{P(nil) \quad \forall a \, \forall x \, (P(x) \to P(cons(a, x)))}{\forall x \, P(x)} \]

Boyer-Moore 的絕招是「從函數的遞迴結構反推出該用的歸納模式」。函數在哪個參數上做 \(nil\) 與 \(cons\) 分案，證明就在哪裡做歸納。

證明器把猜想丟進一座「瀑布」，水流經過層層水池，每一池都是一種化簡啟發式：

水流圖為：

\[ 猜想 \to 化簡 \to 泛化 \to 消去 \to 歸納 \to 子目標 \to 化簡 \to \cdots \]

子目標再送回瀑布頂端，直到全部化為 \(true\) 。人類只需偶爾在半山腰遞一條關鍵引理，剩下的都由水流自動沖刷。

目標： \(append(x, nil) = x\) 。

全程機器自動選了歸納變元 \(x\) ，人類沒有下任何指令。這在 1973 年是爆炸性新聞。

Boyer-Moore 證明器證明了數百條 Lisp 定理，從算術、串列到簡單的作業系統與編譯器正確性，拿下 1980 年代自動推理的半壁江山。

它的結案意義：

歸納公理模式：基例 \(P(nil)\) 加上歸納步 \(P(x) \to P(cons(a, x))\) 可得 \(\forall x \, P(x)\) 。
化簡即重寫： \(append(nil, y)\) 恆重寫為 \(y\) ， \(car(cons(a, x))\) 恆重寫為 \(a\) 。
瀑布五池對照表見上，流程為猜想自頂端流入、子目標迴流的迴圈。

(defun append (x y)
  (if (endp x) y
      (cons (car x) (append (cdr x) y))))
;; 猜想：(equal (append x nil) x)，對 x 做結構歸納