1、代數(shù)等式理論的自動定理證明計算機科學導論第一講,計算機科學技術學院 陳意云,課 程 內 容,課程內容 圍繞學科理論體系中的模型理論, 程序理論和計算理論 1. 模型理論關心的問題 給定模型M，哪些問題可以由模型M解決；如何比較模型的表達能力 2. 程序理論關心的問題 給定模型M，如何用模型M解決問題 包括程序設計范型、程序設計語言、程序設計、形式語義、類型論、程序驗證、程序分析等 3. 計算理論關心的問題 給定模型M和一類問題, 解決該類問題需多少資源,本次講座與這些內容關系不大,課 程 內 容,本講座內容 以代數(shù)等式理論中的定理證明為例，介紹怎樣從中學生熟知的等

2、式演算方法，構造自動定理證明系統(tǒng)，即將問題變?yōu)榭捎糜嬎銠C求解 有助于理解什么是計算思維 計算思維（譯文） 運用計算機科學的基礎概念進行問題求解、系統(tǒng)設計、以及人類行為理解等涵蓋計算機科學之廣度的一系列思維活動,講 座 提 綱,基本知識 代數(shù)項、代數(shù)等式、演繹推理規(guī)則、代數(shù)等式理論、等式定理證明方法 項重寫系統(tǒng) 終止性、良基關系、合流性、局部合流性、關鍵對 良基歸納法 Knuth-Bendix完備化過程,基 本 知 識,代數(shù)項 僅涉及一個類型的代數(shù)項 例：自然數(shù)類型的項0, x, x + 1, x + S(y), f(100, y) 其中x和y變量，f 和S是一階函數(shù)，S是后繼函數(shù) 涉及多個類型

3、的代數(shù)項 若有變量 x : atom, l : list（list是atom的表類型） 并有函數(shù) nil : list, cons : atom list list first : list atom，rest : list list 則 nil, cons(x, l), rest(cons(x, nil), rest(cons(x, l)和cons(first(l), rest(l)都是代數(shù)項,基 本 知 識,代數(shù)等式 例： x + 0 = x，x + S(y) = S(x + y)， x + y = z + 5 first(cons(x, l) = x x : atom, l : list

4、 rest(cons(x, l) = l x : atom, l : list 其中方括號中至少列出等式中出現(xiàn)的變量 等式證明 例：基于一組等式：x + 0 = x和x + S(y) = S(x + y) 怎么證明等式x + S(S(y) = S(S(x + y) ? 需要有推理規(guī)則,等式證明的演繹推理規(guī)則 自反公理：M M 對稱規(guī)則： 傳遞規(guī)則： 加變量規(guī)則： 等價代換規(guī)則：,基 本 知 識,x不在中,P , Q 是類型s的項,等式推理的例子 等價代換規(guī)則： 等式公理：x + 0 = x和x + S(y) = S(x + y) 證明等式： x + S(S(y) = S(S(x + y) 證:

5、 x + S(S(y) 根據x + S(z) = S(x + z)，S(y) = S(y) =S(x + S(y)使用等價代換規(guī)則得到第一個等式 = S(S(x + y) 根據S(z) = S(z), x + S(y) = S(x + y) 使用等價代換規(guī)則得到第二個等式 再利用傳遞規(guī)則可得要證的等式,基 本 知 識,基 本 知 識,代數(shù)等式理論（algebraic equation theory） 在項集T 上從一組等式E(公理、公式)能推出的所 有等式的集合稱為一個等式理論（通俗的解釋） 代數(shù)等式理論的定理證明 判斷等式 M = N 是否在某個代數(shù)等式理論中 常用證明方法 把M和N分別化簡

6、, 若它們的最簡形式一樣則相等 分別證明M和N都等于L 證明MN等于0,還有其它方法,基 本 知 識,哪種證明方法最適合于計算機自動證明？ 把M和N分別化簡, 若它們的最簡形式一樣則相等 若基于所給的等式E，能把M和N化簡到最簡形式，則這種方式相對簡單，便于自動證明 分別證明M和N都等于L 自動選擇L是非常困難的 證明MN等于0 不適用于非數(shù)值類型的項，例如先前給出的atom類型的表,項 重 寫 系 統(tǒng),自動證明要解決的問題 項集T 上等式集E中的等式要定向為單向項重寫規(guī)則, 構成重寫規(guī)則集R, 以方便計算機對項化簡 例如：x + 0 = x，x + S(y) = S(x + y) x 0 =

7、 0，x S(y) = x y + x 定向成如下的項重寫系統(tǒng)R x + 0 x，x + S(y) S(x + y) x 0 0，x S(y) x y + x 記號M N：用一條規(guī)則可將項M歸約成N 例如，x + S(S(y) S(x + S(y) S(S(x + y) 兩步重寫都使用規(guī)則x + S(y) S(x + y),“”既用于規(guī)則，也用于項的歸約,項 重 寫 系 統(tǒng),自動證明要解決的問題 項集T 上等式集E中的等式要定向為單向項重寫規(guī)則, 構成重寫規(guī)則集R, 以方便計算機對項化簡 例如：x + 0 = x，x + S(y) = S(x + y) x 0 = 0，x S(y) = x y

8、 + x 定向成如下的項重寫系統(tǒng)R x + 0 x，x + S(y) S(x + y) x 0 0，x S(y) x y + x 記號M N：用一條規(guī)則可將項M歸約成N 通過定向等式來得到確定同樣代數(shù)理論的重寫系統(tǒng)，需解決三個問題：終止性、合流性和完備性,“”既用于規(guī)則，也用于項的歸約,項 重 寫 系 統(tǒng),終止性 1. 終止性 項集T 上的R不存在無窮歸約序列M0M1M2 , 即: 任何項都能歸約到范式(不能再歸約的項) 2. 有時很難對等式定向，以得到終止的重寫系統(tǒng) 例如：對由三角函數(shù)公式構成的等式系統(tǒng) 和角公式: sin(+) = sin cos + cos sin, 差角公式: sin(

9、 ) = sin cos cos sin, 積化和差: sin cos = (sin(+)+sin()/2, 和差化積: sin+sin = 2sin(+)/2)cos()/2), ,項 重 寫 系 統(tǒng),終止性 3. 定義：良基關系（良基：well-founded） 集合A上的一個關系是良基的，若不存在A上元 素的無窮遞減序列a0 a1 a2 （a b iff b a） 例：自然數(shù)上的關系是良基的，但關系不是 4. 若項集T 和有良基的集合A有映射f :T A, 滿足 T 上任意歸約序列 M0 M1 M2 Mn f f f f A上存在遞減序列 a0 a1 a2 an 則T 上不存在無窮的歸約

10、序列,項 重 寫 系 統(tǒng),終止性 5. 定理 令R是項集T 上的一個重寫系統(tǒng)，若能找到有良基關系的集合A和映射f :T A，使得對R中每條規(guī)則L R都有f (L) f (R) ,那么R是終止的 6. f 的選擇 基于項的語法特點，或者給項指派一種語義 例1（基于語法特點：根據兩邊項語法上的繁簡） first(cons(x, l) x rest(cons(x, l) l,項 重 寫 系 統(tǒng),終止性 例2（邏輯運算系統(tǒng)，給項指派一種語義） x x A N 0, 1 (x y) (x y) A(x, y) = x + y + 1 (x y) (x y) A(x, y) = x y x (y z) (

11、x y) (x z)A(x) = 2x (y z) x (y x) (z x) A表示f 映射算符的結果，它是A上的二元函數(shù) 對每條規(guī)則L R，都有f (L) f (R) 規(guī)則1：x 1, 有 x 規(guī)則2：x, y 1, 有2(x+y+1) = 2x2y2 2x2y,項 重 寫 系 統(tǒng),合流性 1. 記號 MN：M經若干步(含0步)重寫后得到N NM：若有MN M N：若存在P，使得MP且NP 2. 定義 令R是項集T 上的重寫系統(tǒng),若N M P 蘊涵N P，則R是合流的 3. 定義 令R是項集T 上的重寫系統(tǒng),若N M P 蘊涵N P，則R是局部合流的 局部合流關系嚴格弱于合流關系 先考慮局

12、部合流的判定方法，然后再考慮合流,項 重 寫 系 統(tǒng),局部合流性的判定 1. 討論所選用的例子 函數(shù)：nil : listcons : atom list list first : list atom，rest : list list cond : bool list list list 等式： first(cons(x, l) = x, rest(cons(x, l) = l, cons(first(l), rest(l) = l, 下面的討論選擇如下兩條定向后的重寫規(guī)則： rest(cons(x, l) l cons(first(l), rest(l) l,項 重 寫 系 統(tǒng),局部合流性的

13、判定 (1) 無重疊的歸約 歸約規(guī)則： rest(cons(x, l) l （規(guī)則LR） cons(first(l), rest(l) l （規(guī)則LR） 待歸約項： cond (B, rest(cons s l), cons(first(l), rest(l) ) 特點： M中無重疊子項的歸約相互不受影響,項 重 寫 系 統(tǒng),局部合流性的判定 (1) 無重疊的歸約 圖示： LR 和LR是規(guī)則 圖中SL表示代換S作用 于L的結果 代換是變量到項的映射,項 重 寫 系 統(tǒng),局部合流性的判定 (2) 平凡的重疊 歸約規(guī)則： rest(cons(x, l) l（規(guī)則LR） cons(first(l),

14、 rest(l) l（規(guī)則LR） 待歸約項： rest(cons(x, cons(first(l), rest(l) 特點： SL是SL的子項，且S把L中的某變量(這里是l)用 由SL構成的項代換 不同的第1步歸約不會影響局部合流，但合流所 需歸約步數(shù)可能不一樣（取決于R中有幾個l）,項 重 寫 系 統(tǒng),局部合流性的判定 (2) 平凡的重疊 圖示： SL是SL的子項，且S把 L中的某變量x用有SL 構成的項代換 不同的第1步歸約不會影響局部合流，但合流所需 歸約步數(shù)可能不一樣,項 重 寫 系 統(tǒng),局部合流性的判定 (3) 非平凡的重疊 歸約規(guī)則： rest(cons(x, l) l（規(guī)則LR）

15、 cons(first(l),rest(l) l（規(guī)則LR） 待歸約項： rest(cons(first(l), rest(l) 特點： SL在SL的非變量位置 LR 或LR的使用都可能使對方在原定位置 不能使用，故不能保證局部合流,項 重 寫 系 統(tǒng),局部合流性的判定 (3) 非平凡的重疊 圖示： SL在SL的非變量位置 LR或LR的使用都可能使對方在原定位置不 能使用，故不能保證局部合流,項 重 寫 系 統(tǒng),局部合流性的判定 若所有含非平凡重疊的項都能局部合流, 則R也能 把對所有含非平凡重疊的項的檢查縮小為對有限的重寫規(guī)則集的檢查 若由R的重寫規(guī)則確定的所有關鍵對(critical pa

16、ir)都能歸約到同一個項，則所有項的非平凡重疊都能局部合流（可以證明，但在此不深究） 例：重寫規(guī)則 rest(cons(x, l) l，和 cons(first(l), rest(l) l 會形成兩個關鍵對,項 重 寫 系 統(tǒng),第1個關鍵對： 選適當?shù)拇鷵Q，使得兩規(guī)則代換后綠色部分一樣 cons(first(l), rest(l) l rest(cons(x, l) l 第1條規(guī)則中的l用cons(x, l)代換后, 其左部是項： cons(first(cons(x, l), (rest(cons(x, l) 用這兩條規(guī)則化簡上述項可得第1個關鍵對： cons(x, l), cons(firs

17、t(cons(x, l), l) 歸約關鍵對：cons(x, l)已經是范式 cons(first(cons(x, l), l) cons(x, l) 第1個關鍵對能歸約到同一個項,項 重 寫 系 統(tǒng),第2個關鍵對： 選適當?shù)拇鷵Q，使得兩規(guī)則代換后綠色部分一樣 cons(first(l), rest(l) l rest(cons(x, l) l 第2條規(guī)則中的x和l分別代換成first(l)和rest(l)后,其左部是項： rest(cons(first(l), rest(l) 用這兩條規(guī)則化簡上述項可得第2個關鍵對： rest(l), rest(l) 顯然，第2個關鍵對也能歸約到同一個項,項

18、 重 寫 系 統(tǒng),局部合流性的判定 定理 一個重寫系統(tǒng)R是局部合流的，當且僅當對每個關鍵對M, N有M N 如果一個有限的重寫系統(tǒng)R是終止的，那么該定理就給出一個算法，可用于判定R是否局部合流,項 重 寫 系 統(tǒng),局部合流、終止和合流之間的聯(lián)系 定理 令R是終止的重寫系統(tǒng)，那么R是合流的當且僅當它是局部合流的 合流蘊含局部合流 反方向蘊含的證明需要使用良基歸納法,良 基 歸 納 法,良基歸納法 令是集合A上的一個良基關系，令P是A上的某 個性質。若每當所有的P(b) (b a)為真則P(a)為真 (即a.(b.(b a P(b) P(a) )， 那么，對所有的aA，P(a)為真 證明步驟： 歸

19、納基礎: 對任意不存在b使得b a的a，證明P(a) 在不存在b使得b a的情況下， b.(b a P(b) P(a) 等價于 true P(a) 等價于 P(a),良 基 歸 納 法,良基歸納法 令是集合A上的一個良基關系，令P是A上的某 個性質。若每當所有的P(b) (b a)為真則P(a)為真 (即a.(b.(b a P(b) P(a) )， 那么，對所有的aA，P(a)為真 證明步驟： 歸納基礎: 對任意不存在b使得b a的a，證明P(a) 歸納步驟：對任意存在b使得b a的a， b.(b a P(b) P(a)的含義是 假定對所有b a的b，P(b)為真， 然后證明P(a)為真,良

20、基 歸 納 法,良基歸納法 令是集合A上的一個良基關系，令P是A上的某 個性質。若每當所有的P(b) (b a)為真則P(a)為真 (即a.(b.(b a P(b) P(a) )， 那么，對所有的aA，P(a)為真 現(xiàn)在要證明的是：若有M N 和 M P，則N P 若MN, 則規(guī)定N M。 因是終止的系統(tǒng)，因此是良基的。 歸納基礎：若不存在N使得N M，即M是范式， 顯然M具有要證明的性質,良 基 歸 納 法,良基歸納法 令是集合A上的一個良基關系，令P是A上的某 個性質。若每當所有的P(b) (b a)為真則P(a)為真 (即a.(b.(b a P(b) P(a) )， 那么，對所有的aA，

21、P(a)為真 現(xiàn)在要證明的是：若有M N 和 M P，則N P 歸納步驟： 1. 若M N 或 M P是 0步歸約，顯然有N P,良 基 歸 納 法,良基歸納法 令是集合A上的一個良基關系，令P是A上的某 個性質。若每當所有的P(b) (b a)為真則P(a)為真 (即a.(b.(b a P(b) P(a) )， 那么，對所有的aA，P(a)為真 2. 假定M N1 N并且 M P1 P (1) 根據局部合流性， 存在Q，使得N1 Q P1,良 基 歸 納 法,良基歸納法 令是集合A上的一個良基關系，令P是A上的某 個性質。若每當所有的P(b) (b a)為真則P(a)為真 (即a.(b.(b

22、 a P(b) P(a) )， 那么，對所有的aA，P(a)為真 2. 假定M N1 N并且 M P1 P (1) 根據局部合流性， 存在Q，使得N1 Q P1,良 基 歸 納 法,良基歸納法 令是集合A上的一個良基關系，令P是A上的某 個性質。若每當所有的P(b) (b a)為真則P(a)為真 (即a.(b.(b a P(b) P(a) )， 那么，對所有的aA，P(a)為真 2. 假定M N1 N并且 M P1 P (2) 由歸納假設， 存在R， 使得N R Q,良 基 歸 納 法,良基歸納法 令是集合A上的一個良基關系，令P是A上的某 個性質。若每當所有的P(b) (b a)為真則P(a

23、)為真 (即a.(b.(b a P(b) P(a) )， 那么，對所有的aA，P(a)為真 2. 假定M N1 N并且 M P1 P (2) 由歸納假設， 存在R， 使得N R Q,M,良 基 歸 納 法,良基歸納法 令是集合A上的一個良基關系，令P是A上的某 個性質。若每當所有的P(b) (b a)為真則P(a)為真 (即a.(b.(b a P(b) P(a) )， 那么，對所有的aA，P(a)為真 2. 假定M N1 N并且 M P1 P (3) 再由歸納假設， 存在S， 使得R S P,M,良 基 歸 納 法,良基歸納法 令是集合A上的一個良基關系，令P是A上的某 個性質。若每當所有的P

24、(b) (b a)為真則P(a)為真 (即a.(b.(b a P(b) P(a) )， 那么，對所有的aA，P(a)為真 2. 假定M N1 N并且 M P1 P (3) 再由歸納假設， 存在S， 使得R S P (4) N P得證,Knuth-Bendix完備化過程,Knuth-Bendix完備化過程的目的 回顧 最適合于計算機自動證明代數(shù)等式M=N的方式： 把M和N分別化簡, 若它們的最簡形式一樣則相等 由定向代數(shù)等式系統(tǒng)E來得到等價的重寫系統(tǒng)R，需解決三個問題：終止性、合流性和完備性 （完備性在后面的例子中解釋） 完備化過程的目的 為一個代數(shù)等式系統(tǒng)E，構造一個確定同樣代數(shù)理論的終止且合

25、流的重寫系統(tǒng)R,Knuth-Bendix完備化過程,Knuth-Bendix完備化過程簡介 1. 把E定向成一個終止的重寫系統(tǒng)R （若定向失敗，則完備化過程失?。?2. 檢查R的局部合流性并進行完備化 for(R的每個關鍵對M, N) if (不具備M N) 把MN或NM加入R（原因稍后解釋） （若定向失敗，則完備化過程失?。?(過程可能因R不斷地被加入規(guī)則而不終止) 3. 最終的R為所求,Knuth-Bendix完備化過程,例 作為輸入的等式系統(tǒng)E如下 f(x) f(y) = f(x + y) (x + y) + z = x + (y + z) 1. 先定向成一個終止的重寫系統(tǒng)R f(x)

26、f(y) f(x + y) (x + y) + z x + (y + z) 2. 檢查局部合流性并進行完備化,Knuth-Bendix完備化過程,例 作為輸入的等式系統(tǒng)E如下 f(x) f(y) = f(x + y) (x + y) + z = x + (y + z) 1. 先定向成一個終止的重寫系統(tǒng)R f(x) f(y) f(x + y) (x + y) + z x + (y + z) 2. 檢查局部合流性并進行完備化 (1) 把兩條規(guī)則左部的綠色部分進行合一，產生一 個臨界對 f(x + y) + z, f(x) + (f(y) + z) 臨界對的兩個項都已最簡，這個臨界對不能合流,第2條

27、規(guī)則左部的合一結果： (f(x) f(y) + z,Knuth-Bendix完備化過程,例 作為輸入的等式系統(tǒng)E如下 f(x) f(y) = f(x + y) (x + y) + z = x + (y + z) 1. 先定向成一個終止的重寫系統(tǒng)R f(x) f(y) f(x + y) (x + y) + z x + (y + z) 2. 檢查局部合流性并進行完備化 (1) 把兩條規(guī)則左部的綠色部分進行合一，產生一 個臨界對 f(x + y) + z, f(x) + (f(y) + z) (2) 增加重寫規(guī)則f(x + y) + z f(x) + (f(y) + z),第2條規(guī)則左部的合一結果：

28、 (f(x) f(y) + z,Knuth-Bendix完備化過程,例 解釋：增加規(guī)則f(x + y) + z f(x) + (f(y) + z)的原因 在E中可證f(x + y) + z和f(x) + (f(y) + z)相等 等式：f(x) f(y) = f(x + y)和(x + y) + z = x + (y + z) 證明：f(x + y) + z = f(x) f(y) + z = f(x) + (f(y) + z) 在未加上述重寫規(guī)則R中證明不了, 即R不完備： 在R中能證的等式在E中能證，但存在E中能證而在R中不能證的等式 向R中加規(guī)則是為了完備性,Knuth-Bendix完備

29、化過程,例（續(xù)） 1. 先定向成一個終止的重寫系統(tǒng)R f(x) f(y) f(x + y) (x + y) + z x + (y + z) 2. 檢查局部合流性并進行完備化 (1) 產生一個臨界對 f(x + y) + z, f(x) + (f(y) + z) (2) 增加重寫規(guī)則f(x + y) + z f(x) + (f(y) + z) (3) R擴大為： f(x) f(y) f (x + y) (x + y) + z x + (y + z) f(x + y) + z f(x) + (f(y) + z),Knuth-Bendix完備化過程,例（續(xù)） 1. 先定向成一個終止的重寫系統(tǒng)R f(x) f(y) f(x + y) (x + y) + z x + (y + z) 2. 檢查局部合流性并進行完備化 (1) 產