代數(shù)等式理論的自動(dòng)定理證明計(jì)算機(jī)科學(xué)導(dǎo)論第一講(編輯修改稿)
2024-08-14 08:22 本頁面
【文章內(nèi)容簡介】 3. 定義 令 R是項(xiàng)集 T 上的 重寫系統(tǒng) ,若 N ? M ? P 蘊(yùn)涵 N ? ? ? P， 則 R是 局部 合流 的 – 局部合流關(guān)系嚴(yán)格弱于合流關(guān)系 – 先考慮局部合流的判定方法 ， 然后再考慮合流的判定方法 25 項(xiàng) 重 寫 系 統(tǒng) ? 插曲 在介紹局部合流性之前，先介紹代數(shù)項(xiàng)的樹形表示 代數(shù)項(xiàng) cons(first(cons(x, l)), rest(cons(y, l)))的樹形 表示 – 倒長的樹：根在上，葉在下 – 每棵子樹代表一個(gè)子項(xiàng)，整個(gè)樹 代表完整的代數(shù)項(xiàng) 26 cons cons cons rest first y l l x 項(xiàng) 重 寫 系 統(tǒng) ? 局部合流性的判定（問題二的子問題） 1. 討論所選用的例子 函數(shù)： nil : list cons : 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? 27 項(xiàng) 重 寫 系 統(tǒng) ? 局部合流性的判定 （ 問題二的子問題 ） (1) 無重疊的歸約 歸約規(guī)則： rest(cons(x, l)) ? l （ 規(guī)則 L?R） cons(first(l?), rest(l?)) ? l? （ 規(guī)則 L??R?） 待歸約項(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)： M中無重疊子項(xiàng)的歸約相互不受影響 28 項(xiàng) 重 寫 系 統(tǒng) ? 局部合流性的判定 (1) 無重疊的歸約 圖示： – L?R 和 L??R?是規(guī)則 – 圖中 SL和 SR分別表示 代換 S作用于 L的 結(jié)果 S : T ?T – 代換 S的最主要部分 是把變量映射到項(xiàng) M SL SL? M SL SR? M SR SR? SL? M SR 29 cond (B, rest(cons s l), cons(first(l), rest(l))) 項(xiàng) 重 寫 系 統(tǒng) ? 局部合流性的判定 （ 問題二的子問題 ） (2) 平凡的重疊 歸約規(guī)則： rest(cons(x, l)) ? l （ 規(guī)則 L?R） cons(first(l?), rest(l?)) ? l? （ 規(guī)則 L??R?） 待歸約項(xiàng)： rest(cons(x, cons(first(l), rest(l))) ? 方式 1: 原式 ? cons(first(l), rest(l)) ? l ? 方式 2: 原式 ? rest(cons(x, l)) ? l 30 項(xiàng) 重 寫 系 統(tǒng) ? 局部合流性的判定 （ 問題二的子問題 ） (2) 平凡的重疊 歸約規(guī)則： rest(cons(x, l)) ? l （ 規(guī)則 L?R） cons(first(l?), rest(l?)) ? l? （ 規(guī)則 L??R?） 待歸約項(xiàng)： rest(cons(x, cons(first(l), rest(l))) 特點(diǎn)： SL?是 SL的子項(xiàng) ， 且 S把 L中的某變量 (這里是 l)用 由 SL?構(gòu)成的項(xiàng)代換 不同的第 1步歸約不會(huì)影響局部合流 ， 但合流所 需歸約步數(shù)可能不一樣 （ 取決于 R中有幾個(gè) l） 31 項(xiàng) 重 寫 系 統(tǒng) ? 局部合流性的判定 (2) 平凡的重疊 圖示： – SL?是 SL的子項(xiàng) ， 且 S把 L中的某變量 x用有 SL? 構(gòu)成的項(xiàng)代換 – 不同的第 1步歸約 不會(huì)影響局部合流 ， 但合流所需歸約 步數(shù)可能不一樣 SL SL? SL SR? SR SL? SL? SR SR? SR? 32 rest(cons(x, cons(first(l), rest(l))) 項(xiàng) 重 寫 系 統(tǒng) ? 局部合流性的判定 （ 問題二的子問題 ） (3) 非平凡的重疊 歸約規(guī)則： rest(cons(x, l)) ? l （ 規(guī)則 L?R） cons(first(l?), rest(l?))? l? （ 規(guī)則 L??R?） 待歸約項(xiàng)： rest(cons(first(l), rest(l))) ? 方式 1: 原式 ? rest(l) （ 用規(guī)則 L?R） ? 方式 2: 原式 ? rest(l) （ 用規(guī)則 L??R?） 該例比較特殊 ， 都一步歸約就到范式 33 項(xiàng) 重 寫 系 統(tǒng) ? 局部合流性的判定 （ 問題二的子問題 ） (3) 非平凡的重疊 歸約規(guī)則： rest(cons(x, l)) ? l （ 規(guī)則 L?R） cons(first(l?), rest(l?))? l? （ 規(guī)則 L??R?） 待歸約項(xiàng)： rest(cons(first(l), rest(l))) 特點(diǎn)： SL?在 SL的非變量位置 L?R 或 L??R?的使用都可能使 對方在原定位置 不能使用 ， 故不能保證局部合流 34 項(xiàng) 重 寫 系 統(tǒng) ? 局部合流性的判定 (3) 非平凡的重疊 圖示： – SL?在 SL的非變量位置 – L?R或 L??R?的使用 都可能使 對方在原定 位置不能使用 ， 故不 能保證局部合流 SL SL? SL SR? SR ??? ? 35 rest(cons(first(l), rest(l))) 項(xiàng) 重 寫 系 統(tǒng) ? 局部合流性的判定 – 若所有含非平凡重疊的項(xiàng)都能局部合流 , 則 R也能 – 把對所有含非平凡重疊的項(xiàng)的檢查縮小為對有限的重寫規(guī)則集的檢查 若由 R的重寫規(guī)則確定的所有關(guān)鍵對 (critical pair)都能歸約到同一個(gè)項(xiàng) ， 則 所有項(xiàng)的非平凡重疊都能局部合流 （ 課堂上不介紹 ） – 例：重寫規(guī)則 rest(cons(x, l)) ? l， 和 cons(first(l?), rest(l?)) ? l? 會(huì)形成兩個(gè)關(guān)鍵對 36 項(xiàng) 重 寫 系 統(tǒng) 第 1個(gè)關(guān)鍵對： （ 課堂上不介紹 ） – 選適當(dāng)?shù)拇鷵Q ， 使得兩規(guī)則代換后綠色 部分一樣 cons(first(l?), rest(l?)) ? l? rest(cons(x, l)) ? l – 第 1條規(guī)則中的 l?用 cons(x, l)代換后 , 其左部是項(xiàng)： cons(first(cons(x, l)), (rest(cons(x, l))) – 用這兩條規(guī)則化簡上述項(xiàng)可得第 1個(gè)關(guān)鍵對： ? cons(x, l), cons(first(cons(x, l)),
試題試卷相關(guān)推薦
鄂ICP備17016276號(hào)-1