1、泛代數和代數數據類型第1頁，共85頁，2022年，5月20日，10點24分，星期四2.1 引 言代數數據類型包括一個或多個值集一組在這些集合上的函數基本限制是其函數不能有函數變元基本“類型”(type)符號被稱為“類別” (sort)泛代數（也叫做等式邏輯）定義和研究代數數據類型的一般數學框架本章研究泛代數和它在程序設計中定義常用數據類型時的作用 第2頁，共85頁，2022年，5月20日，10點24分，星期四2.1 引 言本章主要內容：代數項和它們在多類別代數中的解釋等式規范（也叫代數規范）和等式證明系統等式證明系統的可靠性和完備性（公理語義和指稱語義的等價）代數之間的同態關系和初始代數數據類

2、型的代數理論從代數規范導出的重寫規則（操作語義）包括了大多數邏輯系統中的一些公共議題第3頁，共85頁，2022年，5月20日，10點24分，星期四2.2 代數、基調和項2.2.1 代數代數一個或多個集合，叫做載體一組特征元素和一階函數，也叫做代數函數f : A1 Ak A例：N N, 0, 1, +, 載體N是自然數集合特征元素0, 1N，也叫做零元函數函數+, : N N N第4頁，共85頁，2022年，5月20日，10點24分，星期四2.2 代數、基調和項多個載體的例子 APCF N, B, 0, 1, , +, true, false, Eq ?, 下面逐步給出代數的一種語法描述，有窮的

3、語法表示在計算機科學中十分重要，可用來定義數據類型證明數據類型的性質還必須討論這種語法描述的指稱語義 滿足一組等式的除了APCF外，可能還有： A5PCF N5, B, 0, 1, 2, 3, 4, +5, true, false, Eq ?, 第5頁，共85頁，2022年，5月20日，10點24分，星期四2.2 代數、基調和項2.2.2 代數項的語法基調 S，FS是一個集合，其元素叫做類別函數符號f : s1 sk s的集合F ，其中表達式s1 sk s叫做f 的類型零元函數符號叫做常量符號例: N S，Fsorts : natfctns : 0, 1 : nat , : nat nat n

4、at 第6頁，共85頁，2022年，5月20日，10點24分，星期四2.2 代數、基調和項項定義基調的目的是用于寫代數項項中可能有變量，因此需假定一個無窮的符號集合V，其元素稱為變量類別指派 x1 : s1, , xk : sk基調S，F和類別指派上類別s的代數項集合Termss (, )定義如下：1、如果x : s ，那么x Termss (, )2、如果f : s1 sk s并且Mi Terms (, ) (i 1, , k)，那么f M1 Mk Termss (, ) 當k 0時，如果f : s，那么f Termss (, )si第7頁，共85頁，2022年，5月20日，10點24分，星

5、期四2.2 代數、基調和項項的例子0, 0 1 Termsnat (N, )0 x Termsnat (N, )，其中 x : nat, 代數項中無約束變元NxM就是簡單地把M中x的每個出現都用N代替記號, x : s x : s引理2.1若MTermss(, , x : s)且NTermss(, )，那么NxMTermss (, )證明 按Termss(, )中項的結構進行歸納第8頁，共85頁，2022年，5月20日，10點24分，星期四2.2 代數、基調和項例用基調stk S, F來寫自然數和自然數棧表達式sorts : nat, stackfctns : 0, 1, 2, : nat ,

6、 : nat nat nat empty : stack push : nat stack stack pop : stack stack top : stack natpush 2 (push 1 (push 0 empty) )是該基調的項第9頁，共85頁，2022年，5月20日，10點24分，星期四2.2 代數、基調和項2.2.3 代數以及項在代數中的解釋基調的代數是為代數項提供含義的數學結構是一個基調，則代數A包含對每個s S，正好有一個載體As一個解釋映射I 把函數I (f ) : A A As 指派給函數符號 f : s1 sk s F把I (f ) As指派給常量符號f : s

7、F N代數N 寫成N N, 0N, 1N, N, N sks1第10頁，共85頁，2022年，5月20日，10點24分，星期四2.2 代數、基調和項代數A的環境 : V s As環境 滿足如果對每個x : s 都有(x)AsM Termss(, )的含義AM是 Ax (x) AM fA (AM1, , AMk)若f : s是常量符號，則Af fA若A清楚時，省略A而直接寫成M不依賴于時，用AM表示M在A中的含義第11頁，共85頁，2022年，5月20日，10點24分，星期四2.2 代數、基調和項例 若(x) 0N x 1 N(x, 1) N (x), 1N) N (0N, 1N) 1N第12頁

8、，共85頁，2022年，5月20日，10點24分，星期四2.2 代數、基調和項例 Astk N, N, 0A, 1A, , A, A, emptyA, pushA, pop A, top AemptyA , 空序列pushA(n, s) n : spopA(n : s) spopA( ) topA(n : s) ntopA( ) 0A若把x:nat映射到自然數3，把s:stack映射到2, 1 pop(push x s) popA(pushA( x , s ) ) popA(pushA(3, 2, 1 ) ) popA( 3, 2, 1 ) 2, 1 第13頁，共85頁，2022年，5月20日

9、，10點24分，星期四2.2 代數、基調和項引理2.2 令A是代數，MTermss(, )，并且是滿足的環境，那么M As證明 根據Termss(, )中項的結構進行歸納引理2.3 令x1, , xk是由出現在MTermss(, )中的所有變量構成的變量表，1和2是滿足的兩個環境, 并且對i1, , k有1(xi) 2(xi), 那么M1 M2證明 基于項結構的歸納第14頁，共85頁，2022年，5月20日，10點24分，星期四2.2 代數、基調和項2.2.4 代換引理引理2.4令MTermss(, , x:s)并且N Termss(, )，那么NxMTermss(, )。并且對任何環境，有

10、NxM M (x a)，其中a N，它是N在下的含義證明 根據項M的結構進行歸納第15頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性代數規范一個基調 + 一組等式調查什么樣的代數滿足這些等式強加的要求使用等式證明系統可推導的新的等式可靠性：從規范可證明的等式在任何滿足該規范的代數中都成立完備性：在滿足規范的所有代數中都成立的等式都可從該規范證明代數規范是描述代數數據類型公理語義的工具第16頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性2.3.1 等式公式 M N ，對某個s，M, N Termss (, ) 若滿足

11、，并且還有M N，則認為代數A在環境下滿足M N ，寫成A, M N 若A在任何環境下都滿足該等式，則寫成 A M N 若代數類C中的任何代數A都滿足該等式，寫成 C M N 若任何一個代數都滿足等式M N ，則寫成 M N(永真的、有效的 )第17頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性平凡的代數若A滿足上所有等式，就說代數A是平凡的例令有兩個類別a和b，令A是一個代數，其中Aa0,1并且Ab A不可能滿足x y x : a, y : a，即下式不成立 A x y x : a, y : a但是A x y x : a, y : a, z : b無意

12、義地成立 第18頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性2.3.2 項代數項代數Terms(, )類別s的載體：集合Termss(, )函數符號f : s1 sk s的解釋I (f ) (M1, , Mk) f M1 Mk項代數Terms(, )的環境也叫做一個代換如果S是代換，則用SM表示同時把M中的各個變量x用Sx替換的結果因此用M表示把代換作用于M的結果第19頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性例類別u函數符號f : u u和g : u u u a : u, b : u, c : uTu a,

13、 b, c, fa, fb, fc, gaa, gab, gac, gbb, , g (f (fa) (f(gbc), 若環境把變量x映射到a，把y映射到f b，則T g(f x) (f y) g(fa) (f (f b)第20頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性引理2.5 令MTerms(, )，并且是滿足的項代數Terms(, )的環境，那么M M證明 對項進行歸納證明從項代數可以知道，只有M和N是語法上相同的項時，等式M N 才會永真第21頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性2.3.3 語

14、義蘊涵和等式證明系統代數規范Spec , E : 基調和一組等式E語義蘊涵：E M N 滿足E的所有代數A都滿足等式M N 語義理論E ：如果E M N 蘊涵M N E代數A的理論Th(A)在A中成立的所有等式的集合這是一個語義理論第22頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性回顧證明系統的可靠性若等式E從一組假設E可證，則E語義上蘊涵E證明系統的完備性若E 語義上蘊涵等式E，則E從E可證下一步先給出代數證明系統，然后討論可靠性和完備性第23頁，共85頁，2022年，5月20日，10點24分，星期四1、語義相等是個等價關系，因此有M M 2、在等式

15、中增加類別指派的規則3、等價代換M = N N = M M = N N = P M = P M = N M = N , x : sM = N , x : s P = Q P/xM = Q/xN 2.3 等式、可靠性和完備性x不在中P , Q Termss(, )第24頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性等式可證若從E中的等式和公理(ref)及推理規則(sym)、(trans)、(subst) 和(add var) 可推出等式M N ，則說該等式可證，寫成 E M N 語法理論如果E M N 蘊涵 M N E E的語法理論Th(E)從E可證的所有

16、等式的集合第25頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性等式集合E是語義一致的若存在某個等式M N ，它不是E的語義蘊涵等式集合E是語法一致的若存在某個等式M N ，它不能由E證明第26頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性例 在基調stk S, F上增加等式top (push x s ) = x s : stack, x : natpop (push x s ) = s s : stack, x : nat 使用這些等式可以證明等式top (push 3 empty ) = 3top(push x

17、s ) = x s : stack, x : nat empty = empty x : nat top(push x empty ) = x x : nat3 = 3 top(push 3 empty ) = 3 第27頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性導出規則 f : s1 sk s Mi, NiTerms (, ) M和N中沒有x, Termss(, )非空M = N N = P P = Q M = Q M1 = N1 Mk = Nk f M1 Mk = f N1 Nk M = N , x : s M = N si第28頁，共85頁，2

18、022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性定理2.6（可靠性）如果E M N ，那么E M N 證明 可以根據該證明的長度進行歸納歸納基礎：長度為1的證明，它是公理或E的一個等式歸納假設：M N 的最后一步是從E1, , En得到，那么，若A E，則A滿足E1, , En要證明：若A滿足最后一條規則的這些前提，則A滿足M N 證明 根據證明規則的集合，分情況進行分析第29頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性命題2.7存在代數理論E和不含x的項M和N，使得E M =N , x : s，但是E M =N 證明令基調有類別

19、a和b，函數符號f : a b和c, d : b令E是包含能從 f x = c x : a和 f x = d x : a證明的所有等式顯然c = d x : a E可以找到一個使等式c = d 不成立的模型a和b對應的分別是空集和多于2個元素的集合由可靠性，c = d 是不可能從E證明的第30頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性例棧代數規范sorts : nat, stackfctns : 0, 1, 2, : nat +, : nat nat nat empty : stack push: nat stack stack pop : stac

20、k stack top : stack nateqns : s : stack; x : nat0 + 0 = 0, 0 + 1 = 1, 0 0 = 0, 0 1 = 0, top (push x s ) = x pop (push x s ) = s第31頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性等式push (top s) (pop s) = s s : stack是不可證的任何形式為top empty = M 的等式都是不可證的，若M是類別為nat的項，并且不含empty第32頁，共85頁，2022年，5月20日，10點24分，星期四2.3

21、等式、可靠性和完備性2.3.4 完備性的形式用于不同邏輯系統的三種不同形式的完備性1、最弱的形式所有的永真公式都是可證的2、演繹完備性每個語義蘊涵在證明系統中都是可推導的3、最小模型完備性每個語法理論都是某個“最小”模型的語義理論對代數來說，最小模型完備性意味著每個語法理論是某個代數A的Th(A) “最小模型”是指它的理論包含的等式最少第33頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性最小模型完備性不一定成立考慮等式E x = y x : a, y : a, z : b 1、a的載體只含一個元素，則E滿足，此時E1 x = y x : a, y : a

22、 成立 2、b的載體為空，則E也滿足，此時E2 z = w z : b, w : b 成立 E1和E2都不是E的語義蘊涵 不存在代數，其理論正好就是由E的等式推論組成的語法理論第34頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性2.3.5 同余、商和演繹完備性同余關系：等價關系加上同余性同余性：指函數保可證明的相等性對單類代數A = A, f1A, f2A, 同余關系是載體A上的等價關系，使得對每個k元函數fA，若aibi(i=1, k)，即ai和bi等價，則fA(a1, , ak ) fA(b1, , bk )對多類代數A = As, I 同余關系是一

23、簇等價關系 s, s AsAs，使得對每個f : s1 sks及變元序列a1, , ak和b1, , bk(ai s bi As ),有fA(a1, , ak ) s fA(b1, , bk )ii第35頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性 A模的商的代數A 把A中有關系元素a a 壓縮成A的一個元素等價類aa a As a a 商代數A定義：(A)s是由As的所有等價類構成的集合Ass as a As函數fA由A的函數fA確定對適當載體的a1, ak，fA (a1, , ak) = fA(a1, , ak)第36頁，共85頁，2022年，5月

24、20日，10點24分，星期四2.3 等式、可靠性和完備性上面定義有意義的條件是fA(a1, , ak)必須只依賴于a1, , ak，而不能依賴于所選的代表a1, , ak例單類別代數N，0，1，上的同余關系“模k等價”這個商代數是眾所周知的整數模k的加結構。如果k等于5，那么3 4 2第37頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性如果是A的一個環境，是一個同余關系，那么A的環境 定義如下： (x) = (x)反過來，對于A的環境，對應它的A的環境有多種選擇引理2.8令是代數A上的同余關系，項MTerms(, )并且是滿足的環境。那么項M在商代數A和

25、環境下的含義(A)M由下式決定(A )M = AM第38頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性引理2.9令E是一組等式集合，令Terms(, )是基調上的項集。由E的可證明性確定的關系E, 是Terms(, )上的同余關系定理2.10（ 完備性）如果E M N ，那么E M N 完備性定理加上可靠性定理表明語法理論和語義理論相同第39頁，共85頁，2022年，5月20日，10點24分，星期四2.3 等式、可靠性和完備性2.3.6 非空類別和最小模型性質沒有空載體的代數有最小模型完備性 類別s非空：集合Termss(, )不是空集對應的載體肯定非空

26、沒有空載體時，可以增加推理規則(nonempty)定理2.11令E是封閉于規則（nonempty）的語法理論，那么存在所有的載體都非空的代數A，使得ETh(A) M = N , x : s M = N 第40頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性2.4.1 同態和同構將同態和同構概念從單類代數推廣到多類代數 同態是從一個代數到另一個代數的保結構的映射從代數A到B的同態h : A B一簇映射h = hs | s S ，使得對的每個函數符號f : s1 sk s，有hs(f A(a1, , ak) ) = f B(hs (a1), , hs (ak) )1k

27、第41頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性例令N = N, 0, 1, ，是模k的等價關系,則把nN映射到它的等價類n是從N到N的一個同態，因為h(0) = 0N = 0h(n + m) = h(n) N h(m) = n + m任何代數到它商代數的同態都用這種方式定義第42頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性例含義函數是從項代數T = Terms(, )到任意代數A的一個同態h : T A。如果是A的一個滿足的環境，該同態的定義是h(M) = AM這是一個同態，因為h (f M1 Mk ) = A f M1

28、Mk = fA(AM1, AMk) = fA(h (M1), , h (Mk) )第43頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性引理2.13令h :AB是任意同態，并且是滿足類別指派的任意A環境。那么對任何項MTerms(, )，有h(AM) = BMh當M中不含變量時，h(AM) =BM證明 基于項的歸納引理2.14如果h :AB和k :B C都是代數的同態，那么合成kh :AC也是代數的同態， (k h)s = ks hs同構 一個雙射的同態, 寫成A B第44頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性2.4.2 初

29、始代數 C是一類代數并且AC，若對每個BC，存在唯一的同態h : AB，則A在C中叫做初始代數初始代數是“典型”的初始代數有盡可能少的非空載體初始代數滿足盡可能少的閉等式AB3B2B1第45頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性例 基調0類別nat，函數符號0 : nat和S : nat nat令C是所有0代數構成的代數類閉項代數T Terms(0, )是C 的初始代數它的載體是所有閉項0, S(0), , Sk(0), 該代數的函數S把Sk(0)映射到Sk1(0)該代數的元素少到能解釋所有的函數符號該代數滿足項之間盡可能少的等式第46頁，共85頁，20

30、22年，5月20日，10點24分，星期四2.4 同態和初始性引理2.15假定h : AB和k : BA都是同態，并且h k = IdB，k h = IdA。那么A和B同構命題2.16若A和B在代數類C中都是初始代數，則A和B同構命題2.17令E是一組等式，且令A=Terms(, )E, 是模可證明的相等性的代數，則A對E來說是初始代數由項代數和商的性質可知，從E可證明的等式在A中都成立還要證明從A到任何滿足E的代數有唯一的同態第47頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性例sorts:natfctns:0 : natS : nat nat : nat na

31、t nat；eqns：x : nat, y : natx + 0 = xx + (Sy) = S(x + y)可以證明如下事實：Sk0 + Sl0 = Sk + l0對任何閉項M，存在某個自然數k，使得M = Sk0第48頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性例x + 0 = xx + (Sy) = S (x + y)可以證明如下事實：等式Sk0 = Sl0是不可證的，除非k = l每個等價類正好包含一個形式為Sk0的項等價類集和形式為Sk0的項集間有一個雙射若把閉項集合0, S0, , Sk0, 作為載體，函數S映射Sk0 Sk10，映射(Sk0, S

32、l0) Skl0，則得一個初始代數這個初始代數和該基調的標準模型（有后繼算子和加法的自然數）同構第49頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性初始代數和其他代數的比較1、和有更多元素的代數比較多余的元素不能由項定義（有垃圾）例1：整數代數Z例2：A = Anat, 0A, SA, +AAnat = (0 N) (1 Z)0A = 0, 0SAi, n = i, n +1i, n +A j, m = max(i, j), n+m第50頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性初始代數和其他代數的比較2、和有較少元素的代數比

33、較一些不能證明為相等的項在該代數中被等同（有混淆）例：模k的自然數第51頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性初始代數的一個重要特點初始代數可能會滿足不能由E證明的額外的等式例：自然數基調例子中，初始代數滿足等式x + y = y + x因為 E M = Sk0和E N = Sl0 蘊涵E M + N = Sk+l0 = N + M第52頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性自然數基調例子中，初始代數滿足等式x + y = y + x不滿足交換律的代數Anat是所有f : X X的函數的集合（X至少有兩個元素）0A

34、是X上的恒等函數，SA是Anat上的恒等映射+A是Anat上的函數合成 A = Anat 0A SA +A滿足E+A沒有交換性，因為函數合成沒有交換性第53頁，共85頁，2022年，5月20日，10點24分，星期四2.4 同態和初始性基項、基代換、基實例（項、等式）如果M N 是Termss(, )的項之間的等式，并且S是一個，基代換，則把SM SN 稱為M N 的基實例命題2.18令E是一組等式，且A對E來說是初始代數，則對任何等式M N ，下面三個條件等價 A滿足M N A滿足M N 的每一個基實例 M N 的每一個基實例都可以從E證明第54頁，共85頁，2022年，5月20日，10點24

35、分，星期四2.5 代數數據類型2.5.1 代數數據類型本節討論數據類型公理化方法的一般特征程序設計中的很多數據類型不存在標準的數學構造，如優先隊列和符號表沒有單一和標準的計算機實現通常是列出它們的操作并公理化地描述這些操作之間的關系因此是公理化地定義而不是由數學構造來定義困難之處：對于一個數據類型，難以斷定是否有了“足夠”的公理第55頁，共85頁，2022年，5月20日，10點24分，星期四2.5 代數數據類型數據抽象的一般原理抽象數據類型由它的規范定義使用這樣數據類型的程序應該只依賴于由它的規范保證的性質，而不依賴于它的任何特定實現一個數據類型的函數可以劃分成構造算子：產生該數據類型的一個新

36、元素運算算子：是該數據類型上的函數，但不產生新的元素觀察算子：應用于該數據類型的元素，但返回其它類型的元素，如自然數或布爾值第56頁，共85頁，2022年，5月20日，10點24分，星期四2.5 代數數據類型 初始代數語義和數據類型歸納代數規范有幾種不同的“語義”形式寬松語義：滿足一個代數規范的所有代數所構成的代數類初始代數語義：滿足一個代數規范的所有初始代數所構成的同構類終結代數語義：滿足一個代數規范的所有終結代數所構成的同構類生成語義：滿足一個代數規范的所有生成代數所構成的代數類第57頁，共85頁，2022年，5月20日，10點24分，星期四2.5 代數數據類型初始代數的性質沒有垃圾沒有混

37、淆支持基于數據類型構造符的歸納構造符集合Spec , E的函數符號集合的子集F0，使得Terms(,)E,的每個等價類正好只含一個由F0的函數符號所構成的基項可以基于對構造符的歸納來證明初始代數的性質第58頁，共85頁，2022年，5月20日，10點24分，星期四2.5 代數數據類型sorts:set, nat, bool 構造符、運算符、觀察符fctns:0, 1, 2, : nat+ : nat nat nat Eq? : nat nat booltrue, false bool empty : setinsert : nat set set union : set set setisme

38、m? : nat set bool condn : bool nat nat nat . . .eqns:x, y : nat, s, s : set, u, v : bool 0 + 0 = 0, 0 +1= 1, 1 +1 = 2, . . . Eq? x x = true Eq? 0 1 = false, Eq? 0 2 = false, . . . ismem? x empty = false ismem? x (insert y s) = if Eq? x y then true else ismem ? x s union empty s = s union (insert y s

39、) s = insert y (union s s) condn true x y = x condn false x y = y . . .第59頁，共85頁，2022年，5月20日，10點24分，星期四2.5 代數數據類型終結代數在一個代數類C中，如果從其中的每個B到其中某個A，都存在唯一的同態，那么代數A是終結代數一個代數類中的所有終結代數都同構若用終結代數作為語義，則稱之為終結語義如果所有載體都是單元素集合的代數也在C中，則這個代數一定是C的終結代數第60頁，共85頁，2022年，5月20日，10點24分，星期四2.5 代數數據類型初始語義和終結語義初始語義：不能證明為相等的就是不相等

40、的終結語義：不能證明為不相等的則是相等的如果把某些類別的解釋固定，而其它類別的解釋用用終結語義，則它是一個有用的方法從初始語義角度看，前面給出的不是集合的規范,而是表的規范。因為不能證明insert x(insert y z)=insert y(insert x z) x: nat, y: nat, z: setinsert x (insert x z) = insert x zx : nat, z : set若用終結語義，且bool的解釋固定,則為集合規范第61頁，共85頁，2022年，5月20日，10點24分，星期四2.5 代數數據類型 解釋沒有意義的項表達式沒有意義的情況除法是一個部分函

41、數，除數為零的表達式沒意義調用不終止的函數也構成一個沒有意義的表達式如果想在代數規范中表示這些情況，必須在基調中增加表示錯誤的項（簡稱錯誤值）怎樣規定這些項的值？有三種可能：什么也不規定任意做一個決定非常仔細地說明什么是所需要的第62頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統 基本定義重寫系統：用于代數項的歸約系統R兩種重要的應用為代數項提供一種計算模型自動定理證明由一組叫做重寫規則(LR)的有向等式組成限制：Var(R) Var(L)由R確定的一步歸約關系RSLxM R SRxM關系R是R的自反傳遞閉包第63頁，共85頁，2022年，5月20日，10點24分，

42、星期四2.6 重寫系統sorts : natfctns : 0 : nat : nat nat + : nat nat nat在這個基調上的一些歸約規則如下：x 0 xx + (x) 0(x y ) z x + (y + z)實例：(x y ) (y) x + (y + (y) x 0 x第64頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統引理2.19（歸約保類別）令R是上的重寫系統，若M Termss(, )且MRN，則N Termss(, ) 如果N M P蘊涵N P，則關系（重寫系統）是合流的若不存在一步歸約的無窮序列M0M1 M2，則關系（重寫系統）是終止的

43、不能再歸約的項稱為范式合流且終止的重寫系統通常又叫做典范系統第65頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統可變換性 若存在M M1 M2 M3 Mk N，則項M, N Termss(, )是可變換的，寫成M R N歸約的無向版本箭頭的方向并沒有什么意義對任何重寫系統，可變換性以及可證明的相等性（把重寫規則看成等式）是一致的第66頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統用自然數的有窮序列來表示項中的位置位置n = 1, 2的子項是hab用M n表示M在位置n的子項用N nM表示M在n的子項由N代換的結果便于引用子項的某個特定出現

44、fggxxhababf (gx(hab)(gba) x第67頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統 合流性和可證明的相等性記號若R是一組重寫規則，ER用來表示對應的無向的等式集合定理2.201、對任何重寫系統R，M RN 當且僅當ER M N；2、對任何合流的重寫系統R，ER M N 當且僅當M R R N第68頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統2.6.3 終止性良基關系集合A上的一個關系是良基的，如果不存在A上元素的無窮遞減序列a0 a1 a2 的話如果能在項和有良基關系的集合A的元素間建立起一個對應，那么可以利用它

45、去證明不存在無窮的歸約序列M0 M1 M2 有幾種方式可把項映射到有良基關系的集合1、利用項的語法特點2、利用代數的語義結構（下面用這種方式）第69頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統代數A = As1, As2, , f1A, f2A, 是良基的，若每個載體As上有一個良基關系s對每個n元函數符號f，如果x1 y1, , xn yn并且對某個i（1 i n）有xi yi，那么fA(x1, , xn) fA(y1, , yn)若A是良基代數，并且M和N都是類別s上的項，若M s N，則寫成A, M N如果對任何環境都有A, M N，那么寫成A M N第70

46、頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統定理2.22令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 yx (y z) (x y) (x z) A(x) = 2x(y z) x (y x) (z x) 各重寫規則的左部定義的值都大于其右部定義的值第71頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統2.6.4 臨界對局部合流 關

47、系是局部合流的，若N M P 蘊涵N P 局部合流關系嚴格弱于合流關系例a bb aa a0b b0a0abb0第72頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統cond B (cdr(cons s l) (cons(car l)(cdr l) )規則如下：cdr(cons x l) lcons(car l)(cdr l) l不相交的歸約MSLSLMSRSLMSLSRMSRSR第73頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統cdr(cons x(cons(car l)(cdr l)規則如下：cdr(cons x l) lcons(c

48、ar l)(cdr l) l平凡的重迭SLSLSLSRSRSLSLSRSRSR第74頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統cdr(cons(car l)(cdr l)規則如下：cdr(cons x l) lcons(car l)(cdr l) l非平凡的重迭SLSLSLSRSR?第75頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統臨界對L R cdr(cons x l) lL R cons(car l)(cdr l) l非平凡重迭是一個三元組SL，SL，m二元組SR，SR mSL叫做臨界對該例有兩個臨界對第一個如下：SL是cdr(cons(car l)(cdr l)臨界對是cdr l, cdr l第76頁，共85頁，2022年，5月20日，10點24分，星期四2.6 重寫系統第二個如下：L R cons(car l)(cdr l) lL R cdr(cons x l) lSL是cons(car (cons x l)(cdr(cons x l)臨界對是cons