跳轉到

1989 年 ACL2：工業級歸納的封山探案#

報案人：Robert Boyer、Matt Kaufmann、J Strother Moore（德州奧斯汀）。 涉案物：一門 Common Lisp 子集。戰績：AMD 與 Motorola 晶片驗證。

案發現場#

1980 年代末，Boyer-Moore 證明器（Nqthm）雖在學界封神， 卻有三個進不了工廠的毛病：

  1. 邏輯是自創的 Lisp 方言，與工業界用的程式語言脫節。
  2. 速度太慢，百萬門級的硬體模型跑不動。
  3. 與編譯器、測試工具鏈不相容，工程師不願重寫模型。

與此同時，AMD 的 K5 浮點除法、Motorola 的 DSP 晶片正為正確性焦頭爛額。 Intel 後來的 Pentium FDIV bug（1994）尚未爆發，但烏雲已在地平線。 工業界需要一台「說工程師語言、跑得動大模型」的證明器。

1989 年，Boyer、Kaufmann、Moore 交出 ACL2（A Computational Logic for Applicative Common Lisp）。 它賭上一切：邏輯即程式語言，證明器即 Lisp。

偵查過程#

線索一：Common Lisp 子集——可執行的邏輯#

ACL2 的絕招是「一語雙用」：同一個函數定義既是邏輯公理， 也是可在 Common Lisp 上直接執行的程式。

(defun app (x y)
  (if (endp x) y
      (cons (car x) (app (cdr x) y))))
(defthm app-assoc
  (equal (app (app a b) c) (app a (app b c))))

\(defun\) 引進遞迴函數（需附終止證明，多用測度 \(measure\) 遞減）， \(defthm\) 宣告定理，證明器自動嘗試證明，失敗則退回給人類補引理。

ACL2 構造 邏輯角色 執行角色
\(defun\) 公理化遞迴函數 可編譯執行的 Lisp
\(defthm\) 待證定理 通過即存為重寫規則
\(encapsulate\) 抽象介面＋約束 模組化驗證
\(measure\) 終止性證據 保證邏輯一致

因為就是 Lisp，ACL2 模型可直接跑測試、跑模擬， 「測試＋證明」在同一語義下無縫銜接，工程師零翻譯成本。

線索二：工業級歸納——瀑布的量產版#

ACL2 繼承 Nqthm 的瀑布模型並工業強化：重寫器更快、 歸納啟發式更準、內建算術決策過程（線性算術、BDD 式推理）。

證明 \(app\) 結合律時，系統自動：

  1. 化簡：展開 \(app\) 定義，消 \(if\) 與 \(car\) 、 \(cdr\) 。
  2. 泛化：把複雜子項抽象為變元 \(z\) ，強化猜想。
  3. 歸納：偵查 \(app\) 在首參數的遞迴模式，對 \(a\) 做 \(nil\) 與 \(cons\) 分案。
  4. 產生的基例 \(app(app(nil, b), c) = app(nil, app(b, c))\) 化簡為 \(app(b, c) = app(b, c)\) 。
  5. 歸納步用歸納假設重寫，證畢。

公式層面仍是結構歸納：

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

不同的是工程：龐大的引理庫、快速重寫、CLOS 級的執行速度， 讓它吞得下百萬項級的硬體模型。

線索三：AMD／Motorola——晶片廠的驗收單#

本案最硬的證據是兩張工業驗收單：

案件 驗證對象 結果
Motorola CAP DSP（1990s） 數位訊號處理器微碼 首個大規模機器驗證的商用晶片之一
AMD K5／Athlon 浮點（1990s-2000s） \(add\) 、 \(div\) 、 \(sqrt\) 微碼與 RTL 抓出模擬沒抓到的角落 bug，後成標準流程
Rockwell、Centaur 等 浮點單元、協定 ACL2 進駐產線

以浮點除法為例，規格是 IEEE-754 的數學定義 \(q = round(a/b)\) ， 實作是迭代微碼。ACL2 證明二者等價，覆蓋一切捨入模式與非規格數。 模擬只能抽樣，證明一次包辦 \(2^{64}\) 種輸入。

結案報告#

ACL2 於 1989 年前後問世，1990 年代打入工業界， 2005 年 Boyer、Kaufmann、Moore 同獲 ACM Software System Award。 它破了「定理證明能否進工廠」的案件，也為第三幕封山。

全幕結案陳詞：1972 年 Prolog 讓邏輯跑起來， 1973 年 Boyer-Moore 讓歸納自動化，1977 年 LCF 立下可信核心、 Pnueli 立下時序規格，1981 年模型檢測舉起窮舉大旗， 1986 年 HOL 與 Isabelle 分頭建城，1988 年 CoC 安上心臟， 1989 年 Coq 與 ACL2 分別以構造與工業之姿出世。 證明，從此工程化。

證據與工具#

  • 終止公式： \(measure(m, x)\) 在每次遞迴嚴格遞減，保證 \(defun\) 邏輯一致。
  • 歸納模式： \(P(nil)\) 與 \(P(x) \to P(cons(a, x))\) 得 \(\forall x \, P(x)\) ，歸納變元由 \(defun\) 的遞迴模式反推。
  • 最小 ACL2 劇本：
(defun app (x y)
  (if (endp x) y (cons (car x) (app (cdr x) y))))
(defthm app-assoc
  (equal (app (app a b) c) (app a (app b c))))
;; :instructions 提示歸納變元 a，觀察瀑布各池輸出
  • 實驗：在 ACL2（或線上 ACL2s）中輸入上例， 觀察證明器自動選的歸納模式，再故意刪去終止測度， 看系統如何拒絕不終止的 \(defun\) ，體會「可執行」與「一致」的綁定。
  • 文獻：Kaufmann 等《Computer-Aided Reasoning: An Approach》， Hunt 等 AMD 浮點驗證報告，Young 等 Motorola CAP 驗證報告。