代數(shù)等式理論的自動(dòng)定理證明計(jì)算機(jī)科學(xué)導(dǎo)論第一講ppt課件

1、代數(shù)等式理論的自動(dòng)定理證明代數(shù)等式理論的自動(dòng)定理證明計(jì)算機(jī)科學(xué)導(dǎo)論第一講計(jì)算機(jī)科學(xué)導(dǎo)論第一講計(jì)算機(jī)科學(xué)技術(shù)學(xué)院計(jì)算機(jī)科學(xué)技術(shù)學(xué)院陳意云陳意 http:/ 程程 內(nèi)內(nèi) 容容 課程內(nèi)容課程內(nèi)容圍繞學(xué)科理論體系中的模型理論圍繞學(xué)科理論體系中的模型理論, 程序理論和計(jì)算理論程序理論和計(jì)算理論1. 模型理論關(guān)心的問(wèn)題模型理論關(guān)心的問(wèn)題 給定模型給定模型m，哪些問(wèn)題可以由模型，哪些問(wèn)題可以由模型m解決；如何解決；如何比較模型的表達(dá)能力比較模型的表達(dá)能力2. 程序理論關(guān)心的問(wèn)題程序理論關(guān)心的問(wèn)題 給定模型給定模型m，如何用模型，如何用模型m解決問(wèn)題解決問(wèn)題 包括程序設(shè)計(jì)范型、程

2、序設(shè)計(jì)語(yǔ)言、程序設(shè)計(jì)、包括程序設(shè)計(jì)范型、程序設(shè)計(jì)語(yǔ)言、程序設(shè)計(jì)、形式語(yǔ)義、類型論、程序驗(yàn)證、程序分析等形式語(yǔ)義、類型論、程序驗(yàn)證、程序分析等3. 計(jì)算理論關(guān)心的問(wèn)題計(jì)算理論關(guān)心的問(wèn)題給定模型給定模型m和一類問(wèn)題和一類問(wèn)題, 解決該類問(wèn)題需多少資源解決該類問(wèn)題需多少資源本次講座基于中學(xué)的等式本次講座基于中學(xué)的等式推理推理, ,與這些內(nèi)容關(guān)系不大與這些內(nèi)容關(guān)系不大2課課 程程 內(nèi)內(nèi) 容容 本講座內(nèi)容本講座內(nèi)容 以以代數(shù)等式理論中的定理證明為例，介紹怎樣從代數(shù)等式理論中的定理證明為例，介紹怎樣從中學(xué)生熟知的等式演算中學(xué)生熟知的等式演算方法方法，構(gòu)造構(gòu)造等式等式定理定理的的自自動(dòng)證明動(dòng)證明系統(tǒng)，即將問(wèn)

3、題變?yōu)橄到y(tǒng)，即將問(wèn)題變?yōu)榭捎糜?jì)算機(jī)求解可用計(jì)算機(jī)求解 有助于理解計(jì)算思維的含義有助于理解計(jì)算思維的含義計(jì)算思維（譯文）計(jì)算思維（譯文） 運(yùn)用計(jì)算機(jī)科學(xué)的基礎(chǔ)概念進(jìn)行問(wèn)題求解、系統(tǒng)運(yùn)用計(jì)算機(jī)科學(xué)的基礎(chǔ)概念進(jìn)行問(wèn)題求解、系統(tǒng)設(shè)計(jì)、以及人類行為理解等涵蓋計(jì)算機(jī)科學(xué)之廣度設(shè)計(jì)、以及人類行為理解等涵蓋計(jì)算機(jī)科學(xué)之廣度的一系列思維活動(dòng)的一系列思維活動(dòng)3講講 座座 提提 綱綱 基本知識(shí)基本知識(shí) 代數(shù)項(xiàng)、代數(shù)等式、演繹推理規(guī)則、代數(shù)等式理代數(shù)項(xiàng)、代數(shù)等式、演繹推理規(guī)則、代數(shù)等式理論、等式定理證明方法論、等式定理證明方法 項(xiàng)重寫系統(tǒng)項(xiàng)重寫系統(tǒng) 終止性、良基關(guān)系、合流性、局部合流性、關(guān)鍵終止性、良基關(guān)系、合流性、

4、局部合流性、關(guān)鍵對(duì)對(duì) 良基歸納法良基歸納法 僅舉例說(shuō)明僅舉例說(shuō)明 knuth-bendix完備化過(guò)程完備化過(guò)程 也僅舉例說(shuō)明也僅舉例說(shuō)明4基基 本本 知知 識(shí)識(shí) 代數(shù)項(xiàng)和代數(shù)等式（僅涉及一個(gè)類型）代數(shù)項(xiàng)和代數(shù)等式（僅涉及一個(gè)類型） 代數(shù)項(xiàng)代數(shù)項(xiàng)例：自然數(shù)類型例：自然數(shù)類型nat 0, 1, 2, : nat常量常量 x, y : nat變量變量 +, f : nat nat nat 二元函數(shù)二元函數(shù) s : nat nat一元的后繼函數(shù)一元的后繼函數(shù) 0, x, x + 1, x + s(y)和和f(100, y) 都是代數(shù)項(xiàng)都是代數(shù)項(xiàng) 代數(shù)等式代數(shù)等式例：例： x + 0 = x，x + s

5、(y) = s(x + y) x + y = z + 55基基 本本 知知 識(shí)識(shí) 代數(shù)項(xiàng)和代數(shù)等式（代數(shù)項(xiàng)和代數(shù)等式（涉及多個(gè)類型涉及多個(gè)類型） 例：定義有限表：同類數(shù)據(jù)的有限序列的集合例：定義有限表：同類數(shù)據(jù)的有限序列的集合 6, 17, 50, 28, 188, 92, 30, 67, 15 18.8, 9.2, 50, 77, 8.6, 5.5, 40.0 a, b, c, d, e, f, , z（非數(shù)值數(shù)據(jù)）（非數(shù)值數(shù)據(jù)） 上述數(shù)據(jù)涉及兩個(gè)類型上述數(shù)據(jù)涉及兩個(gè)類型 序列中元素的類型序列中元素的類型 數(shù)值或非數(shù)值類型數(shù)值或非數(shù)值類型 這些序列所屬的類型，稱為表（這些序列所屬的類型，稱為

6、表（list）類型）類型 非數(shù)值類型非數(shù)值類型 中學(xué)所學(xué)的代數(shù)概念在此已經(jīng)擴(kuò)展中學(xué)所學(xué)的代數(shù)概念在此已經(jīng)擴(kuò)展6基基 本本 知知 識(shí)識(shí) 代數(shù)項(xiàng)和代數(shù)等式（代數(shù)項(xiàng)和代數(shù)等式（涉及多個(gè)類型涉及多個(gè)類型） 代數(shù)項(xiàng)（表代數(shù)項(xiàng)（表類型類型list ，表元類型，表元類型atom） x : atom,l : list 變量變量 nil : list 零元構(gòu)造函數(shù)零元構(gòu)造函數(shù) (常量常量) cons : atom list list 構(gòu)造函數(shù)構(gòu)造函數(shù) first : list atom，rest : list list 觀察函數(shù)觀察函數(shù) nil, cons(x, l), rest(cons(x, nil), r

7、est(cons(x, l), cons(first(l), rest(l)都是代數(shù)項(xiàng)。用都是代數(shù)項(xiàng)。用t 表示項(xiàng)集表示項(xiàng)集 代數(shù)等式代數(shù)等式(方括號(hào)列出等式中出現(xiàn)的變量及類型方括號(hào)列出等式中出現(xiàn)的變量及類型) first(cons(x, l) = x x : atom, l : list rest(cons(x, l) = l x : atom, l : list7基基 本本 知知 識(shí)識(shí) 等式證明等式證明例：基于一組等式（公式、公理）：例：基于一組等式（公式、公理）：x + 0 = x 和和 x + s(y) = s(x + y) 怎么證明等式：怎么證明等式：x + s(s(y) = s(s

8、(x + y) ?需要有推理規(guī)則需要有推理規(guī)則8 等式證明的演繹推理規(guī)則等式證明的演繹推理規(guī)則自反公理：自反公理：m m 對(duì)稱規(guī)則：對(duì)稱規(guī)則：傳遞規(guī)則：傳遞規(guī)則：加變量規(guī)則：加變量規(guī)則：等價(jià)代換規(guī)則：等價(jià)代換規(guī)則：m = n n = m m = n n = p m = p m = n m = n , x : s m = n , x : s p = q p/x m = q/x n 基基 本本 知知 識(shí)識(shí)x不在不在 中中p , q 是類型是類型s的項(xiàng)的項(xiàng)9 等式推理的例子等式推理的例子等價(jià)代換規(guī)則：等價(jià)代換規(guī)則：等式公理：等式公理：x + 0 = x和和x + s(y) = s(x + y)證明等

9、式：證明等式： x + s(s(y) = s(s(x + y)證證明明: x + s(s(y) 根據(jù)根據(jù)x + s(z) = s(x + z)，s(y) = s(y)= s(x + s(y)使用等價(jià)代換規(guī)則得到第一個(gè)等式使用等價(jià)代換規(guī)則得到第一個(gè)等式 s(x + s(y) 根據(jù)根據(jù)s(z) = s(z)，x + s(y) = s(x + y)= s(s(x + y) 使用等價(jià)代換規(guī)則得到第二個(gè)等式使用等價(jià)代換規(guī)則得到第二個(gè)等式x + s(s(y) = s(s(x + y) 根據(jù)根據(jù)傳遞規(guī)則和上面兩等式傳遞規(guī)則和上面兩等式m = n , x : s p = q p/x m = q/x n 基基

10、本本 知知 識(shí)識(shí)10 等式推理的例子等式推理的例子等價(jià)代換規(guī)則：等價(jià)代換規(guī)則：等式公理：等式公理：x + 0 = x和和x + s(y) = s(x + y)證明等式：證明等式： x + s(s(y) = s(s(x + y)證明證明: x + s(s(y)= s(x + s(y) 我們的證明演算習(xí)慣見左邊我們的證明演算習(xí)慣見左邊= s(s(x + y) 它是基于剛才所介紹的演繹推理的它是基于剛才所介紹的演繹推理的若希望計(jì)算機(jī)來(lái)自動(dòng)推理，嚴(yán)格的推理規(guī)則是必若希望計(jì)算機(jī)來(lái)自動(dòng)推理，嚴(yán)格的推理規(guī)則是必須提供的須提供的m = n , x : s p = q p/x m = q/x n 基基 本本 知

11、知 識(shí)識(shí)11基基 本本 知知 識(shí)識(shí) 代數(shù)等式理論（代數(shù)等式理論（algebraic equation theory）在在項(xiàng)集項(xiàng)集t 上上從一組等式從一組等式e（公理）能推出的公理）能推出的所有等式的集合稱為一個(gè)等式理論（通俗的解釋）所有等式的集合稱為一個(gè)等式理論（通俗的解釋） 代數(shù)等式理論的定理證明代數(shù)等式理論的定理證明判斷等式判斷等式 m = n 是否在某個(gè)代數(shù)等式理論中是否在某個(gè)代數(shù)等式理論中 常用證明方法常用證明方法 把把m和和n分別化簡(jiǎn)分別化簡(jiǎn), 若它們的最簡(jiǎn)形式一樣則相等若它們的最簡(jiǎn)形式一樣則相等 分別證明分別證明m和和n都等于都等于l 證明證明m n等于等于0 還有其他方法還有其他

12、方法12基基 本本 知知 識(shí)識(shí) 哪種證明方法最適合于計(jì)算機(jī)自動(dòng)證明？哪種證明方法最適合于計(jì)算機(jī)自動(dòng)證明？ 把把m和和n分別化簡(jiǎn)分別化簡(jiǎn), 若它們的最簡(jiǎn)形式一樣則相等若它們的最簡(jiǎn)形式一樣則相等 若基于等式若基于等式e，通過(guò)等式證明，把，通過(guò)等式證明，把m和和n化簡(jiǎn)到化簡(jiǎn)到最簡(jiǎn)形式，則這種方式相對(duì)簡(jiǎn)單，便于自動(dòng)證明最簡(jiǎn)形式，則這種方式相對(duì)簡(jiǎn)單，便于自動(dòng)證明 并且采用適合于計(jì)算機(jī)使用的單向并且采用適合于計(jì)算機(jī)使用的單向重寫規(guī)則重寫規(guī)則 分別證明分別證明m和和n都等于都等于l 自動(dòng)選擇自動(dòng)選擇l是非常困難的是非常困難的 證明證明m n等于等于0 不適用于非數(shù)值類型的項(xiàng)，例如先前給出的不適用于非數(shù)值類型

13、的項(xiàng)，例如先前給出的atom類型的表類型的表13項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 自動(dòng)證明要解決的問(wèn)題自動(dòng)證明要解決的問(wèn)題 項(xiàng)集項(xiàng)集t 上上等式集等式集e中的等式要定向?yàn)閱蜗蝽?xiàng)重寫中的等式要定向?yàn)閱蜗蝽?xiàng)重寫規(guī)則規(guī)則, 構(gòu)成構(gòu)成重寫規(guī)則集重寫規(guī)則集r, 以方便計(jì)算機(jī)對(duì)項(xiàng)化簡(jiǎn)以方便計(jì)算機(jī)對(duì)項(xiàng)化簡(jiǎn)若若e是：是：x + 0 = x，x + s(y) = s(x + y) x 0 = 0，x s(y) = x y + x定向成如下的項(xiàng)重寫系統(tǒng)定向成如下的項(xiàng)重寫系統(tǒng)rx + 0 x，x + s(y) s(x + y)x 0 0，x s(y) x y + x 記號(hào)記號(hào)m n：用一條規(guī)則可將項(xiàng)：用一條規(guī)則可將項(xiàng)m

14、歸約成歸約成n 若規(guī)則若規(guī)則lr r，含，含z一次出現(xiàn)的項(xiàng)一次出現(xiàn)的項(xiàng)t，以及使得以及使得sl/zt t的代換的代換s，則，則sl/zt sr/zt “”既用于既用于規(guī)則，也用規(guī)則，也用于項(xiàng)的歸約于項(xiàng)的歸約14項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 自動(dòng)證明要解決的問(wèn)題自動(dòng)證明要解決的問(wèn)題 項(xiàng)集項(xiàng)集t 上上等式集等式集e中的等式要定向?yàn)閱蜗蝽?xiàng)重寫中的等式要定向?yàn)閱蜗蝽?xiàng)重寫規(guī)則規(guī)則, 構(gòu)成重寫規(guī)則集構(gòu)成重寫規(guī)則集r, 以方便計(jì)算機(jī)對(duì)項(xiàng)化簡(jiǎn)以方便計(jì)算機(jī)對(duì)項(xiàng)化簡(jiǎn)若若e是：是：x + 0 = x，x + s(y) = s(x + y) x 0 = 0，x s(y) = x y + x定向成如下的項(xiàng)重寫系統(tǒng)定向成

15、如下的項(xiàng)重寫系統(tǒng)rx + 0 x，x + s(y) s(x + y)x 0 0，x s(y) x y + x 記號(hào)記號(hào)m n：用一條規(guī)則可將項(xiàng)：用一條規(guī)則可將項(xiàng)m歸約成歸約成n 例：例：x + s(s(y)“”既用于既用于規(guī)則，也用規(guī)則，也用于項(xiàng)的歸約于項(xiàng)的歸約15項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 自動(dòng)證明要解決的問(wèn)題自動(dòng)證明要解決的問(wèn)題 項(xiàng)集項(xiàng)集t 上上等式集等式集e中的等式要定向?yàn)閱蜗蝽?xiàng)重寫中的等式要定向?yàn)閱蜗蝽?xiàng)重寫規(guī)則規(guī)則, 構(gòu)成重寫規(guī)則集構(gòu)成重寫規(guī)則集r, 以方便計(jì)算機(jī)對(duì)項(xiàng)化簡(jiǎn)以方便計(jì)算機(jī)對(duì)項(xiàng)化簡(jiǎn)若若e是：是：x + 0 = x，x + s(y) = s(x + y) x 0 = 0，x

16、s(y) = x y + x定向成如下的項(xiàng)重寫系統(tǒng)定向成如下的項(xiàng)重寫系統(tǒng)rx + 0 x，x + s(y) s(x + y)x 0 0，x s(y) x y + x 記號(hào)記號(hào)m n：用一條規(guī)則可將項(xiàng)：用一條規(guī)則可將項(xiàng)m歸約成歸約成n 例：例：x + s(s(y) s(x + s(y) s(x + s(y)/zz s(s(x + y)/zz16代換代換s：xx ys(y)項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 自動(dòng)證明要解決的問(wèn)題自動(dòng)證明要解決的問(wèn)題 項(xiàng)集項(xiàng)集t 上上等式集等式集e中的等式要定向?yàn)閱蜗蝽?xiàng)重寫中的等式要定向?yàn)閱蜗蝽?xiàng)重寫規(guī)則規(guī)則, 構(gòu)成重寫規(guī)則集構(gòu)成重寫規(guī)則集r, 以方便計(jì)算機(jī)對(duì)項(xiàng)化簡(jiǎn)以方便計(jì)

17、算機(jī)對(duì)項(xiàng)化簡(jiǎn)若若e是：是：x + 0 = x，x + s(y) = s(x + y) x 0 = 0，x s(y) = x y + x定向成如下的項(xiàng)重寫系統(tǒng)定向成如下的項(xiàng)重寫系統(tǒng)rx + 0 x，x + s(y) s(x + y)x 0 0，x s(y) x y + x 記號(hào)記號(hào)m n：用一條規(guī)則可將項(xiàng)：用一條規(guī)則可將項(xiàng)m歸約成歸約成n 例：例：x + s(s(y) s(x + s(y) s(s(x + y) 子項(xiàng)能與第子項(xiàng)能與第2條規(guī)則的左部匹配條規(guī)則的左部匹配17項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 自動(dòng)證明要解決的問(wèn)題自動(dòng)證明要解決的問(wèn)題 問(wèn)題問(wèn)題1：如何從：如何從e得到得到r，保證項(xiàng)的化簡(jiǎn)能保

18、證項(xiàng)的化簡(jiǎn)能終止終止例：若有規(guī)則例：若有規(guī)則 x + y = y + x，不管怎么定向都有，不管怎么定向都有 a + b b + a a + b 問(wèn)題問(wèn)題2：如何從：如何從e得到得到r，保證對(duì)項(xiàng)采用不同化簡(jiǎn)，保證對(duì)項(xiàng)采用不同化簡(jiǎn)策略所得最簡(jiǎn)項(xiàng)是唯一的（策略所得最簡(jiǎn)項(xiàng)是唯一的（合流性合流性） e： = s( ), eq(x, x) = true, eq(x, s(x) = falser： s( ), eq(x, x) true, eq(x, s(x) false18項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 自動(dòng)證明要解決的問(wèn)題自動(dòng)證明要解決的問(wèn)題 問(wèn)題問(wèn)題1：如何從：如何從e得到得到r，保證項(xiàng)的化簡(jiǎn)能保證項(xiàng)

19、的化簡(jiǎn)能終止終止例：若有規(guī)則例：若有規(guī)則 x + y = y + x，不管怎么定向都有，不管怎么定向都有 a + b b + a a + b 問(wèn)題問(wèn)題2：如何從：如何從e得到得到r，保證對(duì)項(xiàng)采用不同化簡(jiǎn)，保證對(duì)項(xiàng)采用不同化簡(jiǎn)策略所得最簡(jiǎn)項(xiàng)是唯一的（策略所得最簡(jiǎn)項(xiàng)是唯一的（合流性合流性）r： s( ), eq(x, x) true, eq(x, s(x) false則有：則有： eq( , ) true eq( , ) eq( , s( ) false 問(wèn)題問(wèn)題3：如何從：如何從e得到得到r, ,使得使得e和和r確定同樣的代確定同樣的代數(shù)理論，即在數(shù)理論，即在e中能證則在中能證則在r中也能證（中

20、也能證（完備性完備性）19項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 問(wèn)題一：終止性問(wèn)題一：終止性1. 終止性終止性 項(xiàng)集項(xiàng)集t 上的上的r不存在無(wú)窮歸約序列不存在無(wú)窮歸約序列m0m1m2 , 即即: 任何項(xiàng)都能歸約到范式任何項(xiàng)都能歸約到范式(不能再歸約的項(xiàng)不能再歸約的項(xiàng))2. 有時(shí)很難對(duì)等式定向，以得到終止的重寫系統(tǒng)有時(shí)很難對(duì)等式定向，以得到終止的重寫系統(tǒng)例如：對(duì)由三角函數(shù)公式構(gòu)成的等式系統(tǒng)例如：對(duì)由三角函數(shù)公式構(gòu)成的等式系統(tǒng) 和角公式和角公式: sin( + ) = sin cos + cos sin , 差角公式差角公式: sin( ) = sin cos cos sin , 積化和差積化和差: si

21、n cos = (sin( + )+sin()/2, 和差化積和差化積: sin +sin = 2sin( + )/2)cos()/2), 20項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 問(wèn)題一：?jiǎn)栴}一：終止性終止性3. 定義：良基關(guān)系（良基：定義：良基關(guān)系（良基：well-founded）集合集合a上的二元關(guān)系上的二元關(guān)系 是是良基的良基的，若不存在，若不存在a上元上元素的無(wú)窮遞減序列素的無(wú)窮遞減序列a0 a1 a2 （a b iff b a）例：自然數(shù)上的例：自然數(shù)上的1, 有有 x 規(guī)則規(guī)則2： x, y 1, 有有2(x+y+1) = 2x2y2 2x2y22x24項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 問(wèn)題

22、二：合流性問(wèn)題二：合流性1. 記號(hào)記號(hào) mn：m經(jīng)若干步經(jīng)若干步(含含0步步)重寫后得到重寫后得到n nm：若有：若有mn m n：若存在：若存在p，使得，使得mp且且np2. 定義定義 令令r是項(xiàng)集是項(xiàng)集t 上的上的重寫系統(tǒng)重寫系統(tǒng), ,若若n m p 蘊(yùn)涵蘊(yùn)涵n p，則，則r是是合流合流的的3. 定義定義 令令r是項(xiàng)集是項(xiàng)集t 上的上的重寫系統(tǒng)重寫系統(tǒng), ,若若n m p 蘊(yùn)涵蘊(yùn)涵n p，則，則r是是局部局部合流合流的的 局部合流關(guān)系嚴(yán)格弱于合流關(guān)系局部合流關(guān)系嚴(yán)格弱于合流關(guān)系 先考慮局部合流的判定方法，然后再考慮合流的先考慮局部合流的判定方法，然后再考慮合流的判定方法判定方法25項(xiàng)項(xiàng) 重

23、重 寫寫 系系 統(tǒng)統(tǒng) 插曲插曲在介紹局部合流性之前，先介紹代數(shù)項(xiàng)的樹形表示在介紹局部合流性之前，先介紹代數(shù)項(xiàng)的樹形表示代數(shù)項(xiàng)代數(shù)項(xiàng)cons(first(cons(x, l), rest(cons(y, l)的樹形的樹形表示表示 倒長(zhǎng)的樹：根在上，葉在下倒長(zhǎng)的樹：根在上，葉在下 每棵子樹代表一個(gè)子項(xiàng)，整個(gè)樹每棵子樹代表一個(gè)子項(xiàng)，整個(gè)樹代表完整的代數(shù)項(xiàng)代表完整的代數(shù)項(xiàng)26consconsconsrestfirstyllx項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 局部合流性的判定（問(wèn)題二的子問(wèn)題）局部合流性的判定（問(wèn)題二的子問(wèn)題）1. 討論所選用的例子討論所選用的例子函數(shù)：函數(shù)：nil : listcons :

24、 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, 下面的討論針對(duì)如下兩條重寫規(guī)則：下面的討論針對(duì)如下兩條重寫規(guī)則：rest(cons(x, l) lcons(first(l ), rest(l ) l 27項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 局部合流性的判定（問(wèn)題二的子問(wèn)題）局部合流性的判定（問(wèn)題二的子問(wèn)題） (1) 無(wú)重疊的歸約無(wú)重疊的歸約

25、歸約規(guī)則：歸約規(guī)則： rest(cons(x, l) l （規(guī)則（規(guī)則lr） cons(first(l ), rest(l ) l （規(guī)則（規(guī)則lr ） 待歸約項(xiàng)：待歸約項(xiàng)：cond (b, rest(cons s l), cons(first(l), rest(l) ) 方式方式1: 原式原式 cond(b, l, cons(first(l), rest(l) ) cond(b, l, l) 方式方式2: 原式原式 cond (b, rest(cons s l), l) cond(b, l, l) 特點(diǎn)：特點(diǎn)：m中無(wú)重疊子項(xiàng)的歸約相互不受影響中無(wú)重疊子項(xiàng)的歸約相互不受影響28項(xiàng)項(xiàng) 重重 寫寫

26、 系系 統(tǒng)統(tǒng) 局部合流性的判定局部合流性的判定 (1) 無(wú)重疊的歸約無(wú)重疊的歸約圖示：圖示： lr 和和lr 是規(guī)則是規(guī)則 圖中圖中sl和和sr分別表示分別表示 代換代換s作用于作用于l的的 結(jié)果結(jié)果 s : t t 代換代換s的最主要部分的最主要部分是把變量映射到項(xiàng)是把變量映射到項(xiàng)mslsl mslsr msrsr sl msr29cond (b, rest(cons s l), cons(first(l), rest(l)項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 局部合流性的判定（問(wèn)題二的子問(wèn)題）局部合流性的判定（問(wèn)題二的子問(wèn)題） (2) 平凡的重疊平凡的重疊 歸約規(guī)則：歸約規(guī)則：rest(cons(

27、x, l) l（規(guī)則（規(guī)則lr） cons(first(l ), rest(l ) l （規(guī)則（規(guī)則lr ） 待歸約項(xiàng)：待歸約項(xiàng)： rest(cons(x, cons(first(l), rest(l) 方式方式1: 原式原式 cons(first(l), rest(l) l 方式方式2: 原式原式 rest(cons(x, l) l30項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 局部合流性的判定（問(wèn)題二的子問(wèn)題）局部合流性的判定（問(wèn)題二的子問(wèn)題） (2) 平凡的重疊平凡的重疊 歸約規(guī)則：歸約規(guī)則：rest(cons(x, l) l（規(guī)則（規(guī)則lr） cons(first(l ), rest(l ) l （

28、規(guī)則（規(guī)則lr ） 待歸約項(xiàng)：待歸約項(xiàng)： rest(cons(x, cons(first(l), rest(l) 特點(diǎn)：特點(diǎn)：sl 是是sl的子項(xiàng)的子項(xiàng)，且，且s把把l中的某變量中的某變量(這里是這里是l)用用由由sl 構(gòu)成的項(xiàng)代換構(gòu)成的項(xiàng)代換 不同的第不同的第1步歸約不會(huì)影響局部合流，但合流所步歸約不會(huì)影響局部合流，但合流所需歸約步數(shù)可能不一樣（取決于需歸約步數(shù)可能不一樣（取決于r中有幾個(gè)中有幾個(gè)l）31項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 局部合流性的判定局部合流性的判定 (2) 平凡的重疊平凡的重疊 圖示：圖示： sl 是是sl的子項(xiàng)的子項(xiàng)，且，且s把把l中的某變量中的某變量x用有用有sl 構(gòu)成

29、的項(xiàng)代換構(gòu)成的項(xiàng)代換 不同的第不同的第1步歸約步歸約不會(huì)影響局部合流，不會(huì)影響局部合流，但合流所需歸約但合流所需歸約步數(shù)可能不一樣步數(shù)可能不一樣slsl slsr srsl sl srsr sr 32rest(cons(x, cons(first(l), rest(l)項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 局部合流性的判定（問(wèn)題二的子問(wèn)題）局部合流性的判定（問(wèn)題二的子問(wèn)題）(3) 非平凡的重疊非平凡的重疊 歸約規(guī)則：歸約規(guī)則：rest(cons(x, l) l（規(guī)則（規(guī)則lr） cons(first(l ), rest(l ) l （規(guī)則（規(guī)則lr ） 待歸約項(xiàng)：待歸約項(xiàng)：rest(cons(firs

30、t(l), rest(l) 方式方式1: 原式原式 rest(l)（用規(guī)則（用規(guī)則lr） 方式方式2: 原式原式 rest(l)（用規(guī)則（用規(guī)則lr ） 該例比較特殊，都一步歸約就到范式該例比較特殊，都一步歸約就到范式33項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 局部合流性的判定（問(wèn)題二的子問(wèn)題）局部合流性的判定（問(wèn)題二的子問(wèn)題）(3) 非平凡的重疊非平凡的重疊 歸約規(guī)則：歸約規(guī)則：rest(cons(x, l) l（規(guī)則（規(guī)則lr） cons(first(l ), rest(l ) l （規(guī)則（規(guī)則lr ） 待歸約項(xiàng)：待歸約項(xiàng)：rest(cons(first(l), rest(l) 特點(diǎn)：特點(diǎn)：sl 在

31、在sl的非變量位置的非變量位置lr 或或lr 的使用都可能使的使用都可能使對(duì)方在原定位置對(duì)方在原定位置 不能使用，故不能保證局部合流不能使用，故不能保證局部合流34項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 局部合流性的判定局部合流性的判定(3) 非平凡的重疊非平凡的重疊 圖示：圖示： sl 在在sl的非變量位置的非變量位置 lr或或lr 的使用的使用都可能使都可能使對(duì)方在原定對(duì)方在原定位置不能使用，故不位置不能使用，故不能保證局部合流能保證局部合流slsl slsr sr? 35rest(cons(first(l), rest(l)項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 局部合流性的判定局部合流性的判定 若所有含非

32、平凡重疊的項(xiàng)都能局部合流若所有含非平凡重疊的項(xiàng)都能局部合流, 則則r也能也能 把對(duì)所有含非平凡重疊的項(xiàng)的檢查縮小為對(duì)有限把對(duì)所有含非平凡重疊的項(xiàng)的檢查縮小為對(duì)有限的重寫規(guī)則集的檢查的重寫規(guī)則集的檢查 若由若由r的重寫規(guī)則確定的所有關(guān)鍵對(duì)的重寫規(guī)則確定的所有關(guān)鍵對(duì)(critical pair)都能歸約到同一個(gè)項(xiàng)，則都能歸約到同一個(gè)項(xiàng)，則所有項(xiàng)的非平凡重所有項(xiàng)的非平凡重疊都能局部合流疊都能局部合流（課堂上不介紹（課堂上不介紹） 例：重寫規(guī)則例：重寫規(guī)則rest(cons(x, l) l，和，和 cons(first(l ), rest(l ) l 會(huì)形成兩個(gè)關(guān)鍵對(duì)會(huì)形成兩個(gè)關(guān)鍵對(duì)36項(xiàng)項(xiàng) 重重 寫

33、寫 系系 統(tǒng)統(tǒng)第第1個(gè)關(guān)鍵對(duì)：個(gè)關(guān)鍵對(duì)：（課堂上不介紹）（課堂上不介紹） 選適當(dāng)?shù)拇鷵Q，使得兩規(guī)則代換后綠色選適當(dāng)?shù)拇鷵Q，使得兩規(guī)則代換后綠色部分一樣部分一樣cons(first(l ), rest(l ) l rest(cons(x, l) l 第第1條規(guī)則中的條規(guī)則中的l 用用cons(x, l)代換后代換后, 其左部是項(xiàng)：其左部是項(xiàng)：cons(first(cons(x, l), (rest(cons(x, l) 用這兩條規(guī)則化簡(jiǎn)上述項(xiàng)可得第用這兩條規(guī)則化簡(jiǎn)上述項(xiàng)可得第1個(gè)關(guān)鍵對(duì)：個(gè)關(guān)鍵對(duì)： cons(x, l), cons(first(cons(x, l), l) 歸約關(guān)鍵對(duì)：歸約關(guān)鍵對(duì)

34、：cons(x, l)已經(jīng)是范式已經(jīng)是范式 cons(first(cons(x, l), l) cons(x, l) 第第1個(gè)關(guān)鍵對(duì)能歸約到同一個(gè)項(xiàng)個(gè)關(guān)鍵對(duì)能歸約到同一個(gè)項(xiàng)37項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng)第第2個(gè)關(guān)鍵對(duì)：個(gè)關(guān)鍵對(duì)：（課堂上不介紹）（課堂上不介紹） 選適當(dāng)?shù)拇鷵Q，使得兩規(guī)則代換后綠色選適當(dāng)?shù)拇鷵Q，使得兩規(guī)則代換后綠色部分一樣部分一樣 cons(first(l ), rest(l ) l rest(cons(x, l) l 第第2條規(guī)則中的條規(guī)則中的x和和l分別代換成分別代換成first(l )和和rest(l )后后,其左部是項(xiàng)：其左部是項(xiàng)：rest(cons(first(l )

35、, rest(l ) 用這兩條規(guī)則化簡(jiǎn)上述項(xiàng)可得第用這兩條規(guī)則化簡(jiǎn)上述項(xiàng)可得第2個(gè)關(guān)鍵對(duì)：個(gè)關(guān)鍵對(duì)： rest(l ), rest(l ) 顯然，第顯然，第2個(gè)關(guān)鍵對(duì)也能歸約到同一個(gè)項(xiàng)個(gè)關(guān)鍵對(duì)也能歸約到同一個(gè)項(xiàng)38項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)統(tǒng) 局部合流性的判定局部合流性的判定 定理定理 一個(gè)重寫系統(tǒng)一個(gè)重寫系統(tǒng)r是局部合流的，當(dāng)且僅當(dāng)對(duì)是局部合流的，當(dāng)且僅當(dāng)對(duì)每個(gè)關(guān)鍵對(duì)每個(gè)關(guān)鍵對(duì) m, n 有有m n 如果如果一個(gè)有限的重寫系統(tǒng)一個(gè)有限的重寫系統(tǒng)r是終止的，那么該定是終止的，那么該定理就給出一個(gè)算法，可用于判定理就給出一個(gè)算法，可用于判定r是否局部合流是否局部合流39項(xiàng)項(xiàng) 重重 寫寫 系系 統(tǒng)

36、統(tǒng) 局部合流、終止和合流之間的聯(lián)系局部合流、終止和合流之間的聯(lián)系定理定理 令令r是終止的重寫系統(tǒng)，那么是終止的重寫系統(tǒng)，那么r是合流的當(dāng)是合流的當(dāng)且僅當(dāng)它是局部合流的且僅當(dāng)它是局部合流的 合流蘊(yùn)含局部合流（這是顯然的）合流蘊(yùn)含局部合流（這是顯然的） 反方向蘊(yùn)含的證明需要使用良基歸納法反方向蘊(yùn)含的證明需要使用良基歸納法40良良 基基 歸歸 納納 法法 良基歸納法良基歸納法用一個(gè)簡(jiǎn)單例子說(shuō)明它比自然數(shù)歸納法更一般用一個(gè)簡(jiǎn)單例子說(shuō)明它比自然數(shù)歸納法更一般證明：對(duì)任何自然數(shù)的有限集合，每次刪除一個(gè)元證明：對(duì)任何自然數(shù)的有限集合，每次刪除一個(gè)元 素，最終會(huì)到達(dá)空集素，最終會(huì)到達(dá)空集 1. 若忽略集合中元

37、素的個(gè)性，只關(guān)心集合中元素若忽略集合中元素的個(gè)性，只關(guān)心集合中元素的個(gè)數(shù)，則可以用自然數(shù)歸納法的個(gè)數(shù)，則可以用自然數(shù)歸納法 2. 若關(guān)注元素個(gè)性（雖無(wú)必要）若關(guān)注元素個(gè)性（雖無(wú)必要） ：集合之間的歸約：集合之間的歸約規(guī)則規(guī)則: x1, , xnx2, , xn其中其中x1是左邊集合的任意元素是左邊集合的任意元素 3.良基關(guān)系：良基關(guān)系：a b則則a b410, 1, 21, 20, 20, 1012良良 基基 歸歸 納納 法法 良基歸納法良基歸納法需要證明：任何自然數(shù)的有限集合可歸約到空集需要證明：任何自然數(shù)的有限集合可歸約到空集1. 對(duì)所有的歸約路徑進(jìn)行歸納對(duì)所有的歸約路徑進(jìn)行歸納2. 良基

38、歸納證明良基歸納證明歸納基礎(chǔ)：歸納基礎(chǔ)：經(jīng)經(jīng)0步歸約到步歸約到歸納假設(shè)：對(duì)所有的歸納假設(shè)：對(duì)所有的s s1, s s2, s sn, s1, s2, , sn都能歸約都能歸約到到歸納證明：證明歸納證明：證明s能歸約到能歸約到420, 1, 21, 20, 20, 1012良良 基基 歸歸 納納 法法 良基歸納法良基歸納法（課堂上不介紹）（課堂上不介紹）令令 是集合是集合a上的一個(gè)良基關(guān)系，令上的一個(gè)良基關(guān)系，令p是是a上的某上的某個(gè)性質(zhì)。若每當(dāng)所有的個(gè)性質(zhì)。若每當(dāng)所有的p(b) (b a)為真則為真則p(a)為真為真(即即 a.( b.(b a p(b) p(a) )，那么，對(duì)所有的那么，對(duì)所

39、有的a a，p(a)為真為真證明步驟：證明步驟： 歸納基礎(chǔ)歸納基礎(chǔ): 對(duì)任意不存在對(duì)任意不存在b使得使得b a的的a，證明，證明p(a) 在不存在在不存在b使得使得b a的情況下，的情況下， b.(b a p(b) p(a)等價(jià)于等價(jià)于 true p(a)等價(jià)于等價(jià)于 p(a)43良良 基基 歸歸 納納 法法 良基歸納法良基歸納法（課堂上不介紹）（課堂上不介紹）令令 是集合是集合a上的一個(gè)良基關(guān)系，令上的一個(gè)良基關(guān)系，令p是是a上的某上的某個(gè)性質(zhì)。若每當(dāng)所有的個(gè)性質(zhì)。若每當(dāng)所有的p(b) (b a)為真則為真則p(a)為真為真(即即 a.( b.(b a p(b) p(a) )，那么，對(duì)所有的

40、那么，對(duì)所有的a a，p(a)為真為真證明步驟：證明步驟： 歸納基礎(chǔ)歸納基礎(chǔ): 對(duì)任意不存在對(duì)任意不存在b使得使得b a的的a，證明，證明p(a) 歸納步驟：對(duì)任意存在歸納步驟：對(duì)任意存在b使得使得b a的的a， b.(b a p(b) p(a)在此得出歸納假設(shè)：在此得出歸納假設(shè)： 假定對(duì)所有假定對(duì)所有b a的的b，p(b)為真，然后證明：為真，然后證明： 歸納證明：證明歸納證明：證明p(a)為真為真44良良 基基 歸歸 納納 法法 用良基歸納法證明合流性用良基歸納法證明合流性證明：若有證明：若有m n和和 m p，則，則n p若若mn, 則規(guī)定則規(guī)定n m。因系統(tǒng)終止因系統(tǒng)終止, 故故 是良

41、基的是良基的歸納基礎(chǔ)：歸納基礎(chǔ)： 若不存在若不存在n使得使得n m，即即m是范式，顯然是范式，顯然m具有具有要證明的性質(zhì)要證明的性質(zhì) 因?yàn)橐驗(yàn)閙只能只能0步歸約到步歸約到m本身，圖上的本身，圖上的n和和p都只都只能是能是mmnp45(m)(m)m良良 基基 歸歸 納納 法法 用良基歸納法證明合流性用良基歸納法證明合流性證明：若有證明：若有m n和和 m p，則，則n p若若mn, 則規(guī)定則規(guī)定n m。因系統(tǒng)終止因系統(tǒng)終止, 故故 是良基的是良基的歸納步驟：歸納步驟：假定假定m n1 n并且并且m p1 p(1) 根據(jù)局部合流性，根據(jù)局部合流性，存在存在q，使得，使得n1 q p1mn1p1np

42、46良良 基基 歸歸 納納 法法 用良基歸納法證明合流性用良基歸納法證明合流性證明：若有證明：若有m n和和 m p，則，則n p若若mn, 則規(guī)定則規(guī)定n m。因系統(tǒng)終止因系統(tǒng)終止, 故故 是良基的是良基的歸納步驟：歸納步驟： 假定假定m n1 n并且并且m p1 p(1) 根據(jù)局部合流性，根據(jù)局部合流性，存在存在q，使得，使得n1 q p1mn1p1qnp47良良 基基 歸歸 納納 法法 用良基歸納法證明合流性用良基歸納法證明合流性證明：若有證明：若有m n和和 m p，則，則n p若若mn, 則規(guī)定則規(guī)定n m。因系統(tǒng)終止因系統(tǒng)終止, 故故 是良基的是良基的歸納步驟：歸納步驟： 假定假定

43、m n1 n并且并且m p1 p(2) 由歸納假設(shè)，由歸納假設(shè)，存在存在r， 使得使得n r qmn1p1qnp48良良 基基 歸歸 納納 法法 用良基歸納法證明合流性用良基歸納法證明合流性證明：若有證明：若有m n和和 m p，則，則n p若若mn, 則規(guī)定則規(guī)定n m。因系統(tǒng)終止因系統(tǒng)終止, 故故 是良基的是良基的歸納步驟：歸納步驟： 假定假定m n1 n并且并且m p1 p(2) 由歸納假設(shè)，由歸納假設(shè)，存在存在r， 使得使得n r qmn1p1qnrp49良良 基基 歸歸 納納 法法 用良基歸納法證明合流性用良基歸納法證明合流性證明：若有證明：若有m n和和 m p，則，則n p若若m

44、n, 則規(guī)定則規(guī)定n m。因系統(tǒng)終止因系統(tǒng)終止, 故故 是良基的是良基的歸納步驟：歸納步驟： 假定假定m n1 n并且并且m p1 p(3) 再由歸納假設(shè)，再由歸納假設(shè)，存在存在s， 使得使得r s pmn1p1qnrp50良良 基基 歸歸 納納 法法 用良基歸納法證明合流性用良基歸納法證明合流性證明：若有證明：若有m n和和 m p，則，則n p若若mn, 則規(guī)定則規(guī)定n m。因系統(tǒng)終止因系統(tǒng)終止, 故故 是良基的是良基的歸納步驟：歸納步驟： 假定假定m n1 n并且并且m p1 p(3) 再由歸納假設(shè)，再由歸納假設(shè)，存在存在s， 使得使得r s p(4) n p得證得證mn1p1qnrsp

45、51knuth-bendix完備化過(guò)程完備化過(guò)程 問(wèn)題三：完備性問(wèn)題三：完備性回顧回顧 最適合于計(jì)算機(jī)自動(dòng)證明代數(shù)等式最適合于計(jì)算機(jī)自動(dòng)證明代數(shù)等式m=n的方式：的方式： 把把m和和n分別化簡(jiǎn)分別化簡(jiǎn), 若它們的最簡(jiǎn)形式一樣則相等若它們的最簡(jiǎn)形式一樣則相等 由定向代數(shù)等式系統(tǒng)由定向代數(shù)等式系統(tǒng)e來(lái)得到等價(jià)的重寫系統(tǒng)來(lái)得到等價(jià)的重寫系統(tǒng)r，需解決三個(gè)問(wèn)題：終止性、合流性和完備性需解決三個(gè)問(wèn)題：終止性、合流性和完備性完備性：從完備性：從e可可得到得到r，e和和r確定同樣的代數(shù)理論確定同樣的代數(shù)理論 概要介紹概要介紹knuth-bendix完備化過(guò)程完備化過(guò)程 給出一個(gè)完備化過(guò)程不終止的例子。由此可

46、知，給出一個(gè)完備化過(guò)程不終止的例子。由此可知，并非對(duì)任何并非對(duì)任何e都都可以得到與之有同樣代數(shù)理論的可以得到與之有同樣代數(shù)理論的r52knuth-bendix完備化過(guò)程完備化過(guò)程 knuth-bendix完備化過(guò)程的目的完備化過(guò)程的目的完備化過(guò)程的目的完備化過(guò)程的目的 為一個(gè)代數(shù)等式系統(tǒng)為一個(gè)代數(shù)等式系統(tǒng)e，構(gòu)造一個(gè)確定同樣代數(shù)，構(gòu)造一個(gè)確定同樣代數(shù)理論的終止且合流的重寫系統(tǒng)理論的終止且合流的重寫系統(tǒng)r53knuth-bendix完備化過(guò)程完備化過(guò)程 knuth-bendix完備化過(guò)程簡(jiǎn)介完備化過(guò)程簡(jiǎn)介1. 把把e定向成一個(gè)終止的重寫系統(tǒng)定向成一個(gè)終止的重寫系統(tǒng)r（若定向失敗，則完備化過(guò)程失敗

47、）（若定向失敗，則完備化過(guò)程失?。?. 檢查檢查r的局部合流性并進(jìn)行完備化的局部合流性并進(jìn)行完備化for(r的每個(gè)關(guān)鍵對(duì)的每個(gè)關(guān)鍵對(duì) m, n ) if (不具備不具備m n) 把把mn或或nm加入加入r（原因稍后解釋）（原因稍后解釋） （若定向失敗，則完備化過(guò)程失?。ㄈ舳ㄏ蚴?，則完備化過(guò)程失敗） (過(guò)程可能因過(guò)程可能因r不斷地被加入規(guī)則而不終止不斷地被加入規(guī)則而不終止)3. 最終的最終的r為所求為所求54knuth-bendix完備化過(guò)程完備化過(guò)程 例：完備化過(guò)程不終止例：完備化過(guò)程不終止作為輸入的等式系統(tǒng)作為輸入的等式系統(tǒng)e如下如下f(x) f(y) = f(x + y)(x + y)

48、 + z = x + (y + z)1. 先定向成一個(gè)終止的重寫系統(tǒng)先定向成一個(gè)終止的重寫系統(tǒng)r f(x) f(y) f(x + y) (x + y) + z x + (y + z)2. 檢查局部合流性并進(jìn)行完備化檢查局部合流性并進(jìn)行完備化55knuth-bendix完備化過(guò)程完備化過(guò)程 例：完備化過(guò)程不終止例：完備化過(guò)程不終止作為輸入的等式系統(tǒng)作為輸入的等式系統(tǒng)e如下如下f(x) f(y) = f(x + y)(x + y) + z = x + (y + z)1. 先定向成一個(gè)終止的重寫系統(tǒng)先定向成一個(gè)終止的重寫系統(tǒng)r f(x) f(y) f(x + y) (x + y) + z x + (

49、y + z)2. 檢查局部合流性并進(jìn)行完備化檢查局部合流性并進(jìn)行完備化(1) 把兩條規(guī)則左部的綠色部分進(jìn)行合一，把兩條規(guī)則左部的綠色部分進(jìn)行合一，產(chǎn)生產(chǎn)生一一個(gè)個(gè)臨界臨界對(duì)對(duì) f(x + y) + z, f(x) + (f(y) + z) 臨界對(duì)的兩個(gè)項(xiàng)都已最簡(jiǎn)，這個(gè)臨界對(duì)不能合流臨界對(duì)的兩個(gè)項(xiàng)都已最簡(jiǎn)，這個(gè)臨界對(duì)不能合流 因第因第2條規(guī)則左部的合條規(guī)則左部的合一結(jié)果：一結(jié)果： (f(x) f(y) + z 56knuth-bendix完備化過(guò)程完備化過(guò)程 例：完備化過(guò)程不終止例：完備化過(guò)程不終止作為輸入的等式系統(tǒng)作為輸入的等式系統(tǒng)e如下如下f(x) f(y) = f(x + y)(x + y

50、) + z = x + (y + z)1. 先定向成一個(gè)終止的重寫系統(tǒng)先定向成一個(gè)終止的重寫系統(tǒng)r f(x) f(y) f(x + y) (x + y) + z x + (y + z)2. 檢查局部合流性并進(jìn)行完備化檢查局部合流性并進(jìn)行完備化(1) 把兩條規(guī)則左部的綠色部分進(jìn)行合一，把兩條規(guī)則左部的綠色部分進(jìn)行合一，產(chǎn)生產(chǎn)生一一個(gè)個(gè)臨界臨界對(duì)對(duì) f(x + y) + z, f(x) + (f(y) + z) (2) 增加增加重寫規(guī)則重寫規(guī)則f(x + y) + z f(x) + (f(y) + z) 因第因第2條規(guī)則左部的合條規(guī)則左部的合一結(jié)果：一結(jié)果： (f(x) f(y) + z 57kn

51、uth-bendix完備化過(guò)程完備化過(guò)程 例：完備化過(guò)程不終止例：完備化過(guò)程不終止解釋：增加規(guī)則解釋：增加規(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ī)則在未加上述重寫規(guī)則r中證明不了中證明不了, 即即r不不完備完備： 在在r中能證的等式在中能證的

52、等式在e中中能證，但存在能證，但存在e中中能證而能證而在在r中不能證的等式中不能證的等式 向向r中加規(guī)則是為了完備性中加規(guī)則是為了完備性58knuth-bendix完備化過(guò)程完備化過(guò)程 例（續(xù)）例（續(xù)）1. 先定向成一個(gè)終止的重寫系統(tǒng)先定向成一個(gè)終止的重寫系統(tǒng)r f(x) f(y) f(x + y) (x + y) + z x + (y + z)2. 檢查局部合流性并進(jìn)行完備化檢查局部合流性并進(jìn)行完備化(1) 產(chǎn)生一個(gè)臨界對(duì)產(chǎn)生一個(gè)臨界對(duì) f(x + y) + z, f(x) + (f(y) + z) (2) 增加重寫規(guī)則增加重寫規(guī)則f(x + y) + z f(x) + (f(y) + z)(3) r擴(kuò)大為：擴(kuò)大為： f(x) f(y) f (x + y) (x + y) + z x + (y + z) f(x + y) + z f(x) + (f(y) + z)59knuth-bendix完備化過(guò)程完備化過(guò)程 例（續(xù)）例（續(xù)）1. 先定向成一個(gè)終止的重寫系統(tǒng)先定向成一個(gè)終止的重寫系統(tǒng)r