第3章泛代數和代數數據類型-資料下載頁

　　

【正文】 g g x x h a b a b f (gx(hab))(gba) x 重寫系統 合流性和可證明的相等性 記號 如果 R是一組重寫規則 ， ER用來表示對應的無向的等式集合 定理 對任何重寫系統 R， M?R N???當且僅當ER M ? N??? 對任何合流的重寫系統 R， ER M ? N???當且僅當 M ?? R ? ?? R N 重寫系統 終止性 ? 良基關系：集合 A上的一個關系 ?是 良基的 ，如果不存在 A上元素的無窮遞減序列 a0 ? a1 ? a2 ?… 的話 。 ? 如果能在項和有良基關系的集合 A的元素間建立起一個對應 ， 那么可以利用它去證明不存在無窮的歸約序列 M0 ? M1 ? M2 ? … ? 有幾種方式可把項映射到有良基關系的集合 – 利用代數的語義結構 重寫系統 ? 代數 A = ? As1, As2, … , f1A, f2A, … ?是良基的 ，如果 – 每個載體 As上有一個良基關系 ?s – 對每個 n元函數符號 f， 如果 x1 ? y1, … , xn ? yn并且對某個 i（ 1? i ? n） 有 xi ? yi， 那么 f A(x1, … , xn) ? f A(y1, … , yn) ? 若 A是一個良基代數 ， 并且 M和 N都是類別 s上的項 ， 如果 〖 M〗 ? ?s 〖 N〗 ?， 那么寫成 A， ? M ? N – 如果對任何環境 ?都有 A， ? M ? N， 那么寫成A M ? N。 重寫系統 ? 定理 令 R是 ?項上的一個重寫系統 ， 并且令 A是一個良基的 ?代數 。 如果對 R中每條規則 L ? R有 A L ? R， 那么 R是終止的 ? 例 ?? x ? x 載體 Abool? 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) ? (x ? y) ? (x ? z) ?A(x) = 2x (y ? z) ? x ? (y ? x) ? (z ? x) 每條重寫規則的左部定義的值都大于其右部定義的值 重寫系統 臨界對 ? 局部合流 關系 ?是局部合流的 ， 如果 N ? M ? P蘊涵 N ?? ? ?? P – 局部合流關系嚴格弱于合流關系 – 例 a ? b, b ? a a ? a0, b ? b0 a0 a b b0 重寫系統 cond B (cdr(cons s l)) (cons(car l?)(cdr l?) ) 規則如下： cdr(cons x l) ? l cons(car l?)(cdr l?) ? l? 不相交的歸約 M SL SL? M SR SL?? M SL SR? M SR SR? 重寫系統 cdr(cons x(cons(car l?)(cdr l?))) 規則如下： cdr(cons x l) ? l cons(car l?)(cdr l?) ? l? 平凡的重迭 SL SL? SL SR? SR SL? SL? SR SR? SR? 重寫系統 cdr(cons(car l?)(cdr l?)) 規則如下： cdr(cons x l) ? l cons(car l?)(cdr l?) ? l? 非平凡的重迭 SL SL? SL SR? SR ??? 重寫系統 ? 臨界對 – L ? R cdr(cons x l) ? l – L? ? R? cons(car l?)(cdr l?) ? l? – 非平凡重迭是一個三元組 ?SL， SL?， m?? – 二元組 ?SR， ?SR?? m? ?SL?叫做 臨界對 – 該例有兩個臨界對 ， 第一個如下： – SL是 cdr(cons(car l)(cdr l)) – 臨界對是 ?cdr l, cdr l? 重寫系統 – 第二個如下： – L ? R cons(car l?)(cdr l?) ? l? – L? ? R? cdr(cons x l) ? l – SL是 cons(car (cons x l))(cdr(cons x l)) – 臨界對是 ?cons x l, cons (car (cons x l)) l? ? 若 f (gxy) ? R?， L中有子項 f z、 f (gPQ)、 f (h … )。 f (h … )不可能與 f (gxy) 合一 ? 同一條規則的兩次使用可能引起重迭 ， 如 – f (f x) ? a f (f (f x)) ? 左部完全相同的情況 ： L ? R和 L ? R? 重寫系統 命題 一個重寫系統 R是局部合流的 ， 當且僅當對每個臨界對 ?M, N?有 M ?? R ? ?? R N 證明 – 從左到右的蘊涵是簡單明了的 – 另一個方向的證明仿照用于啟發臨界對定義的推理：不相交 、 平凡的重迭 、 臨界對的代換實例 ? 如果一個有限的重寫系統 R是終止的 ， 那么該命題就給出一個算法 ， 可用于判定 R是否局部合流 重寫系統 左線性無重迭重寫系統 ? 無重迭：沒有非平凡的臨界對 無重迭的重寫系統不一定是合流的 例如： ? ? S ? Eq ? x x ? true Eq ? x (S x) ? false Eq ? ? ?有兩個不同的范式 Eq ? ? ? ? true Eq ? ? ? ? Eq ? ? (S ?) ? false 重寫系統 ? 左線性的規則： 任何變量在規則的左部的出現不超過一次的話 ? 左線性的系統： 每一條規則都是左線性的 ? 命題 如果 R是左線性和無重迭的 ， 那么??R是合流的 ? 例 下面是一個 左線性無重迭重寫系統 car (cons x l) ? x cdr (cons x l) ? l isempty? nil ? true isempty? (cons x l) ? false 加入非左線性規則 cons (car l) (cdr l) ? l 后不合流 isempty? (cons (car l) (cdr l))有兩個范式 重寫系統 局部合流 、 終止和合流之間的聯系 命題 令 R是終止的重寫系統 ， 那么 R是合流的當且僅當它是局部合流的 良基歸納 令 ?是集合 A上的一個良基關系 ， 令 P是 A上的某個性質 。 若每當 所有的 P(b) (b ? a)為真則 P(a)為真 (?a. (?b.( b ? a ? P(b)) ? P(a)) )， 那么 ， 對所有的 a?A， P(a)為真 。 M N1 P1 Q N R S P 重寫系統 局部合流 、 終止和合流之間的聯系 命題 令 R是終止的重寫系統 ， 那么 R是合流的當且僅當它是局部合流的 例 if true then x else y ? x if false then x else y ? y if u then x else x ? x M N1 P1 Q N R S P 重寫系統 KnuthBendix完備化過程 ? 一組等式 – fx ? f y = f (x + y) – (x + y) + z = x + (y + z) ? 構造一個確定同樣代數理論的終止且合流的重寫系統 – 先定向成一個重寫系統 fx ? f y ? f (x + y) (x + y) + z ? x + (y + z) 重寫系統 – 產生一個臨界對 ?f (x + y) + z, f x + (f y + z )? – 增加一條重寫規則 fx ? f y ? f (x + y) (x + y) + z ? x + (y + z) f (x + y) + z ? f x + (f y + z ) – 本例增加無數條重寫規則 f n (x + y) + z ? f nx + (f n y + z ) 習 題 第一次： (a)， 第二次： ， ， 第三次： (d), (e)， 第四次： ， 第五次： (a)，