1、第2章 泛代數(shù)和代數(shù)數(shù)據(jù)類型,函數(shù)式程序設(shè)計(jì)語(yǔ)言PCF由三部分組成 代數(shù)數(shù)據(jù)類型：自然數(shù)類型和布爾類型 帶函數(shù)和積等類型的純類型化演算 不動(dòng)點(diǎn)算子 第2章到第4章對(duì)這三部分進(jìn)行透徹的研究 本章研究像自然數(shù)類型和布爾類型這樣的代數(shù)數(shù)據(jù)類型,2.1 引 言,代數(shù)數(shù)據(jù)類型包括 一個(gè)或多個(gè)值集 一組在這些集合上的函數(shù) 基本限制是其函數(shù)不能有函數(shù)變?cè)?基本“類型”(type)符號(hào)被稱為“類別” (sort) 泛代數(shù)（也叫做等式邏輯） 定義和研究代數(shù)數(shù)據(jù)類型的一般數(shù)學(xué)框架 本章研究泛代數(shù)和它在程序設(shè)計(jì)中定義常用數(shù)據(jù)類型時(shí)的作用,2.1 引 言,本章主要內(nèi)容： 代數(shù)項(xiàng)和它們?cè)诙囝悇e代數(shù)中的解釋 等式規(guī)范（也

2、叫代數(shù)規(guī)范）和等式證明系統(tǒng) 等式證明系統(tǒng)的可靠性和完備性（公理語(yǔ)義和指稱語(yǔ)義的等價(jià)） 代數(shù)之間的同態(tài)關(guān)系和初始代數(shù) 數(shù)據(jù)類型的代數(shù)理論 從代數(shù)規(guī)范導(dǎo)出的重寫規(guī)則（操作語(yǔ)義） 包括了大多數(shù)邏輯系統(tǒng)中的一些公共議題,2.2 代數(shù)、基調(diào)和項(xiàng),2.2.1 代數(shù) 代數(shù) 一個(gè)或多個(gè)集合，叫做載體 一組特征元素和一階函數(shù)，也叫做代數(shù)函數(shù) f : A1 Ak A 例：N N, 0, 1, +, 載體N是自然數(shù)集合 特征元素0, 1N，也叫做零元函數(shù) 函數(shù)+, : N N N,2.2 代數(shù)、基調(diào)和項(xiàng),多個(gè)載體的例子 APCF N, B, 0, 1, , +, true, false, Eq ?, 下面逐步給出代

3、數(shù)的一種語(yǔ)法描述，有窮的語(yǔ)法表示在計(jì)算機(jī)科學(xué)中十分重要，可用來 定義數(shù)據(jù)類型 證明數(shù)據(jù)類型的性質(zhì) 還必須討論這種語(yǔ)法描述的指稱語(yǔ)義 滿足一組等式的除了APCF外，可能還有： A5PCF N5, B, 0, 1, 2, 3, 4, +5, true, false, Eq ?, ,2.2 代數(shù)、基調(diào)和項(xiàng),2.2.2 代數(shù)項(xiàng)的語(yǔ)法 基調(diào) S，F(xiàn) S是一個(gè)集合，其元素叫做類別 函數(shù)符號(hào)f : s1 sk s的集合F ，其中表達(dá)式s1 sk s叫做f 的類型 零元函數(shù)符號(hào)叫做常量符號(hào) 例: N S，F(xiàn) sorts : nat fctns : 0, 1 : nat , : nat nat nat,2.2

4、代數(shù)、基調(diào)和項(xiàng),項(xiàng) 定義基調(diào)的目的是用于寫代數(shù)項(xiàng) 項(xiàng)中可能有變量，因此需假定一個(gè)無窮的符號(hào)集合V，其元素稱為變量 類別指派 x1 : s1, , xk : sk 基調(diào)S，F(xiàn)和類別指派上類別s的代數(shù)項(xiàng)集合Termss (, )定義如下： 1、如果x : s ，那么x Termss (, ) 2、如果f : s1 sk s并且Mi Terms (, ) (i 1, , k)，那么f M1 Mk Termss (, ) 當(dāng)k 0時(shí)，如果f : s，那么f Termss (, ),si,2.2 代數(shù)、基調(diào)和項(xiàng),項(xiàng)的例子 0, 0 1 Termsnat (N, ) 0 x Termsnat (N, )，

5、其中 x : nat, 代數(shù)項(xiàng)中無約束變?cè)?NxM就是簡(jiǎn)單地把M中x的每個(gè)出現(xiàn)都用N代替 記號(hào), x : s x : s 引理2.1 若MTermss(, , x : s)且NTermss(, )，那么NxMTermss (, ) 證明 按Termss(, )中項(xiàng)的結(jié)構(gòu)進(jìn)行歸納,2.2 代數(shù)、基調(diào)和項(xiàng),例 用基調(diào)stk S, F來寫自然數(shù)和自然數(shù)棧表達(dá)式 sorts : nat, stack fctns : 0, 1, 2, : nat , : nat nat nat empty : stack push : nat stack stack pop : stack stack top : st

6、ack nat push 2 (push 1 (push 0 empty) )是該基調(diào)的項(xiàng),2.2 代數(shù)、基調(diào)和項(xiàng),2.2.3 代數(shù)以及項(xiàng)在代數(shù)中的解釋 基調(diào)的代數(shù)是為代數(shù)項(xiàng)提供含義的數(shù)學(xué)結(jié)構(gòu) 是一個(gè)基調(diào)，則代數(shù)A包含 對(duì)每個(gè)s S，正好有一個(gè)載體As 一個(gè)解釋映射I 把函數(shù)I (f ) : A A As 指派給函數(shù)符號(hào) f : s1 sk s F 把I (f ) As指派給常量符號(hào)f : s F N代數(shù)N 寫成 N N, 0N, 1N, N, N ,sk,s1,2.2 代數(shù)、基調(diào)和項(xiàng),代數(shù)A的環(huán)境 : V s As 環(huán)境 滿足 如果對(duì)每個(gè)x : s 都有(x)As M Termss(, )的

7、含義AM是 Ax (x) AM fA (AM1, , AMk) 若f : s是常量符號(hào)，則Af fA 若A清楚時(shí)，省略A而直接寫成M 不依賴于時(shí)，用AM表示M在A中的含義,2.2 代數(shù)、基調(diào)和項(xiàng),例 若(x) 0N x 1 N(x, 1) N (x), 1N) N (0N, 1N) 1N,2.2 代數(shù)、基調(diào)和項(xiàng),例 Astk N, N, 0A, 1A, , A, A, emptyA, pushA, pop A, top A emptyA , 空序列pushA(n, s) n : s popA(n : s) spopA( ) topA(n : s) ntopA( ) 0A 若把x:nat映射到自

8、然數(shù)3，把s:stack映射到2, 1 pop(push x s) popA(pushA( x , s ) ) popA(pushA(3, 2, 1 ) ) popA( 3, 2, 1 ) 2, 1,2.2 代數(shù)、基調(diào)和項(xiàng),引理2.2 令A(yù)是代數(shù)，MTermss(, )，并且是滿足 的環(huán)境，那么M As 證明 根據(jù)Termss(, )中項(xiàng)的結(jié)構(gòu)進(jìn)行歸納 引理2.3 令x1, , xk是由出現(xiàn)在MTermss(, )中的所有 變量構(gòu)成的變量表，1和2是滿足的兩個(gè)環(huán)境, 并 且對(duì)i1, , k有1(xi) 2(xi), 那么M1 M2 證明 基于項(xiàng)結(jié)構(gòu)的歸納,2.2 代數(shù)、基調(diào)和項(xiàng),2.2.4 代

9、換引理 引理2.4 令MTermss(, , x:s)并且N Termss(, )，那 么NxMTermss(, )。并且對(duì)任何環(huán)境，有 NxM M (x a)， 其中a N，它是N在下的含義 證明 根據(jù)項(xiàng)M的結(jié)構(gòu)進(jìn)行歸納,2.3 等式、可靠性和完備性,代數(shù)規(guī)范 一個(gè)基調(diào) + 一組等式 調(diào)查什么樣的代數(shù)滿足這些等式強(qiáng)加的要求 使用等式證明系統(tǒng)可推導(dǎo)的新的等式 可靠性：從規(guī)范可證明的等式在任何滿足該規(guī)范的代數(shù)中都成立 完備性：在滿足規(guī)范的所有代數(shù)中都成立的等式都可從該規(guī)范證明 代數(shù)規(guī)范是描述代數(shù)數(shù)據(jù)類型公理語(yǔ)義的工具,2.3 等式、可靠性和完備性,2.3.1 等式 公式 M N ，對(duì)某個(gè)s，M,

10、 N Termss (, ) 若滿足，并且還有M N，則認(rèn)為代數(shù)A在環(huán)境下滿足M N ，寫成 A, M N 若A在任何環(huán)境下都滿足該等式，則寫成 A M N 若代數(shù)類C中的任何代數(shù)A都滿足該等式，寫成 C M N 若任何一個(gè)代數(shù)都滿足等式M N ，則寫成 M N(永真的、有效的 ),2.3 等式、可靠性和完備性,平凡的代數(shù) 若A滿足上所有等式，就說代數(shù)A是平凡的 例 令有兩個(gè)類別a和b，令A(yù)是一個(gè)代數(shù)，其中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無意義地成立,2.

11、3 等式、可靠性和完備性,2.3.2 項(xiàng)代數(shù) 項(xiàng)代數(shù)Terms(, ) 類別s的載體：集合Termss(, ) 函數(shù)符號(hào)f : s1 sk s的解釋 I (f ) (M1, , Mk) f M1 Mk 項(xiàng)代數(shù)Terms(, )的環(huán)境也叫做一個(gè)代換 如果S是代換，則用SM表示同時(shí)把M中的各個(gè)變量x用Sx替換的結(jié)果 因此用M表示把代換作用于M的結(jié)果,2.3 等式、可靠性和完備性,例 類別u 函數(shù)符號(hào)f : u u和g : u u u a : u, b : u, c : u Tu a, b, c, fa, fb, fc, gaa, gab, gac, gbb, , g (f (fa) (f(gbc)

12、, 若環(huán)境把變量x映射到a，把y映射到f b，則 T g(f x) (f y) g(fa) (f (f b),2.3 等式、可靠性和完備性,引理2.5 令MTerms(, )，并且是滿足的項(xiàng)代數(shù) Terms(, )的環(huán)境，那么M M 證明 對(duì)項(xiàng)進(jìn)行歸納證明 從項(xiàng)代數(shù)可以知道，只有M和N是語(yǔ)法上相同的項(xiàng)時(shí)，等式M N 才會(huì)永真,2.3 等式、可靠性和完備性,2.3.3 語(yǔ)義蘊(yùn)涵和等式證明系統(tǒng) 代數(shù)規(guī)范Spec , E : 基調(diào)和一組等式E 語(yǔ)義蘊(yùn)涵：E M N 滿足E的所有代數(shù)A都滿足等式M N 語(yǔ)義理論E ： 如果E M N 蘊(yùn)涵M N E 代數(shù)A的理論Th(A) 在A中成立的所有等式的集合

13、這是一個(gè)語(yǔ)義理論,2.3 等式、可靠性和完備性,回顧 證明系統(tǒng)的可靠性 若等式E從一組假設(shè)E可證，則E語(yǔ)義上蘊(yùn)涵E 證明系統(tǒng)的完備性 若E 語(yǔ)義上蘊(yùn)涵等式E，則E從E可證 下一步 先給出代數(shù)證明系統(tǒng)，然后討論可靠性和完備性,1、語(yǔ)義相等是個(gè)等價(jià)關(guān)系，因此有 M M 2、在等式中增加類別指派的規(guī)則 3、等價(jià)代換,2.3 等式、可靠性和完備性,x不在中,P , Q Termss(, ),2.3 等式、可靠性和完備性,等式可證 若從E中的等式和公理(ref)及推理規(guī)則(sym)、 (trans)、(subst) 和(add var) 可推出等式M N ， 則說該等式可證，寫成 E M N 語(yǔ)法理論

14、如果E M N 蘊(yùn)涵 M N E E的語(yǔ)法理論Th(E) 從E可證的所有等式的集合,2.3 等式、可靠性和完備性,等式集合E是語(yǔ)義一致的 若存在某個(gè)等式M N ，它不是E的語(yǔ)義蘊(yùn)涵 等式集合E是語(yǔ)法一致的 若存在某個(gè)等式M N ，它不能由E證明,2.3 等式、可靠性和完備性,例 在基調(diào)stk S, F上增加等式 top (push x s ) = x s : stack, x : nat pop (push x s ) = s s : stack, x : nat 使用這些等式可以證明等式 top (push 3 empty ) = 3,2.3 等式、可靠性和完備性,導(dǎo)出規(guī)則 f : s1 s

15、k s Mi, NiTerms (, ) M和N中沒有x, Termss(, )非空,si,2.3 等式、可靠性和完備性,定理2.6（可靠性） 如果E M N ，那么E M N 證明 可以根據(jù)該證明的長(zhǎng)度進(jìn)行歸納 歸納基礎(chǔ)：長(zhǎng)度為1的證明，它是公理或E的一個(gè)等式 歸納假設(shè)：M N 的最后一步是從E1, , En得到，那么，若A E，則A滿足E1, , En 要證明：若A滿足最后一條規(guī)則的這些前提，則A滿足M N 證明 根據(jù)證明規(guī)則的集合，分情況進(jìn)行分析,2.3 等式、可靠性和完備性,命題2.7 存在代數(shù)理論E和不含x的項(xiàng)M和N，使得 E M =N , x : s，但是E M =N 證明 令基調(diào)

16、有類別a和b，函數(shù)符號(hào)f : a b和c, d : b 令E是包含能從 f x = c x : a和 f x = d x : a證明的所有等式 顯然c = d x : a E 可以找到一個(gè)使等式c = d 不成立的模型 a和b對(duì)應(yīng)的分別是空集和多于2個(gè)元素的集合 由可靠性，c = d 是不可能從E證明的,2.3 等式、可靠性和完備性,例 棧代數(shù)規(guī)范 sorts : nat, stack fctns : 0, 1, 2, : nat +, : nat nat nat empty : stack push: nat stack stack pop : stack stack top : stack

17、 nat eqns : s : stack; x : nat 0 + 0 = 0, 0 + 1 = 1, 0 0 = 0, 0 1 = 0, top (push x s ) = x pop (push x s ) = s,2.3 等式、可靠性和完備性,等式 push (top s) (pop s) = s s : stack 是不可證的 任何形式為 top empty = M 的等式都是不可證的，若M是類別為nat的項(xiàng)，并且 不含empty,2.3 等式、可靠性和完備性,2.3.4 完備性的形式 用于不同邏輯系統(tǒng)的三種不同形式的完備性 1、最弱的形式 所有的永真公式都是可證的 2、演繹完備性

18、每個(gè)語(yǔ)義蘊(yùn)涵在證明系統(tǒng)中都是可推導(dǎo)的 3、最小模型完備性 每個(gè)語(yǔ)法理論都是某個(gè)“最小”模型的語(yǔ)義理論 對(duì)代數(shù)來說，最小模型完備性意味著每個(gè)語(yǔ)法理論是某個(gè)代數(shù)A的Th(A) “最小模型”是指它的理論包含的等式最少,2.3 等式、可靠性和完備性,最小模型完備性不一定成立 考慮等式 E x = y x : a, y : a, z : b 1、a的載體只含一個(gè)元素，則E滿足，此時(shí) E1 x = y x : a, y : a 成立 2、b的載體為空，則E也滿足，此時(shí) E2 z = w z : b, w : b 成立 E1和E2都不是E的語(yǔ)義蘊(yùn)涵 不存在代數(shù)，其理論正好就是由E的等式推論 組成的語(yǔ)法理論,

19、2.3 等式、可靠性和完備性,2.3.5 同余、商和演繹完備性 同余關(guān)系：等價(jià)關(guān)系加上同余性 同余性：指函數(shù)保可證明的相等性 對(duì)單類代數(shù)A = A, f1A, f2A, 同余關(guān)系是載體A上的等價(jià)關(guān)系，使得對(duì)每個(gè)k元函數(shù)fA，若aibi(i=1, k)，即ai和bi等價(jià)，則fA(a1, , ak ) fA(b1, , bk ) 對(duì)多類代數(shù)A = As, I 同余關(guān)系是一簇等價(jià)關(guān)系 s, s AsAs，使得對(duì)每個(gè)f : s1 sks及變?cè)蛄衋1, , ak和b1, , bk(ai s bi As ),有fA(a1, , ak ) s fA(b1, , bk ),i,i,2.3 等式、可靠性和完備

20、性,A模的商的代數(shù)A 把A中有關(guān)系元素a a 壓縮成A的一個(gè)元素 等價(jià)類a a a As a a 商代數(shù)A定義： (A)s是由As的所有等價(jià)類構(gòu)成的集合 Ass as a As 函數(shù)fA由A的函數(shù)fA確定 對(duì)適當(dāng)載體的a1, ak， fA (a1, , ak) = fA(a1, , ak),2.3 等式、可靠性和完備性,上面定義有意義的條件是 fA(a1, , ak)必須只依賴于a1, , ak，而不能依賴于所選的代表a1, , ak 例 單類別代數(shù)N，0，1，上的同余關(guān)系“模k等價(jià)” 這個(gè)商代數(shù)是眾所周知的整數(shù)模k的加結(jié)構(gòu)。如果k等于5，那么3 4 2,2.3 等式、可靠性和完備性,如果是A

21、的一個(gè)環(huán)境，是一個(gè)同余關(guān)系，那么A的環(huán)境 定義如下： (x) = (x) 反過來，對(duì)于A的環(huán)境，對(duì)應(yīng)它的A的環(huán)境有多種選擇 引理2.8 令是代數(shù)A上的同余關(guān)系，項(xiàng)MTerms(, ) 并且是滿足的環(huán)境。那么項(xiàng)M在商代數(shù)A和環(huán) 境下的含義(A)M由下式?jīng)Q定 (A )M = AM,2.3 等式、可靠性和完備性,引理2.9 令E是一組等式集合，令Terms(, )是基調(diào)上 的項(xiàng)集。由E的可證明性確定的關(guān)系E, 是Terms(, )上的同余關(guān)系 定理2.10（ 完備性） 如果E M N ，那么E M N 完備性定理加上可靠性定理表明語(yǔ)法理論和語(yǔ)義理論相同,2.3 等式、可靠性和完備性,2.3.6 非空

22、類別和最小模型性質(zhì) 沒有空載體的代數(shù)有最小模型完備性 類別s非空：集合Termss(, )不是空集 對(duì)應(yīng)的載體肯定非空 沒有空載體時(shí)，可以增加推理規(guī)則(nonempty) 定理2.11 令E是封閉于規(guī)則（nonempty）的語(yǔ)法理論，那 么存在所有的載體都非空的代數(shù)A，使得ETh(A),2.4 同態(tài)和初始性,2.4.1 同態(tài)和同構(gòu) 將同態(tài)和同構(gòu)概念從單類代數(shù)推廣到多類代數(shù) 同態(tài)是從一個(gè)代數(shù)到另一個(gè)代數(shù)的保結(jié)構(gòu)的映射 從代數(shù)A到B的同態(tài)h : A B 一簇映射h = hs | s S ，使得對(duì)的每個(gè)函數(shù)符號(hào)f : s1 sk s，有 hs(f A(a1, , ak) ) = f B(hs (a1

23、), , hs (ak) ),1,k,2.4 同態(tài)和初始性,例 令N = N, 0, 1, ，是模k的等價(jià)關(guān)系,則把nN 映射到它的等價(jià)類n是從N到N的一個(gè)同態(tài)， 因?yàn)?h(0) = 0N = 0 h(n + m) = h(n) N h(m) = n + m 任何代數(shù)到它商代數(shù)的同態(tài)都用這種方式定義,2.4 同態(tài)和初始性,例 含義函數(shù)是從項(xiàng)代數(shù)T = Terms(, )到任意代數(shù) A的一個(gè)同態(tài)h : T A。如果是A的一個(gè)滿足 的環(huán)境，該同態(tài)的定義是 h(M) = AM 這是一個(gè)同態(tài)，因?yàn)?h (f M1 Mk ) = A f M1 Mk = fA(AM1, AMk) = fA(h (M1),

24、 , h (Mk) ),2.4 同態(tài)和初始性,引理2.13 令h :AB是任意同態(tài)，并且是滿足類別指派 的任意A環(huán)境。那么對(duì)任何項(xiàng)MTerms(, )，有 h(AM) = BMh 當(dāng)M中不含變量時(shí)，h(AM) =BM 證明 基于項(xiàng)的歸納 引理2.14 如果h :AB和k :B C都是代數(shù)的同態(tài)，那么 合成kh :AC也是代數(shù)的同態(tài)， (k h)s = ks hs 同構(gòu) 一個(gè)雙射的同態(tài), 寫成A B,2.4 同態(tài)和初始性,2.4.2 初始代數(shù) C是一類代數(shù)并且AC，若對(duì)每個(gè)BC，存在唯一的同態(tài)h : AB，則A在C中叫做初始代數(shù) 初始代數(shù)是“典型”的 初始代數(shù)有盡可能少的非空載體 初始代數(shù)滿足盡

25、可能少的閉等式,2.4 同態(tài)和初始性,例 基調(diào)0 類別nat， 函數(shù)符號(hào)0 : nat和S : nat nat 令C是所有0代數(shù)構(gòu)成的代數(shù)類 閉項(xiàng)代數(shù)T Terms(0, )是C 的初始代數(shù) 它的載體是所有閉項(xiàng)0, S(0), , Sk(0), 該代數(shù)的函數(shù)S把Sk(0)映射到Sk1(0) 該代數(shù)的元素少到能解釋所有的函數(shù)符號(hào) 該代數(shù)滿足項(xiàng)之間盡可能少的等式,2.4 同態(tài)和初始性,引理2.15 假定h : AB和k : BA都是同態(tài)，并且 h k = IdB，k h = IdA。那么A和B同構(gòu) 命題2.16 若A和B在代數(shù)類C中都是初始代數(shù)，則A和B同構(gòu) 命題2.17 令E是一組等式，且令A(yù)=

26、Terms(, )E, 是模 可證明的相等性的代數(shù)，則A對(duì)E來說是初始代數(shù) 由項(xiàng)代數(shù)和商的性質(zhì)可知，從E可證明的等式在A中都成立 還要證明從A到任何滿足E的代數(shù)有唯一的同態(tài),2.4 同態(tài)和初始性,例 sorts:nat fctns:0 : natS : nat nat : nat nat nat； eqns：x : nat, y : nat x + 0 = x x + (Sy) = S(x + y) 可以證明如下事實(shí)： Sk0 + Sl0 = Sk + l0 對(duì)任何閉項(xiàng)M，存在某個(gè)自然數(shù)k，使得M = Sk0,2.4 同態(tài)和初始性,例x + 0 = x x + (Sy) = S (x + y)

27、 可以證明如下事實(shí)： 等式Sk0 = Sl0是不可證的，除非k = l 每個(gè)等價(jià)類正好包含一個(gè)形式為Sk0的項(xiàng) 等價(jià)類集和形式為Sk0的項(xiàng)集間有一個(gè)雙射 若把閉項(xiàng)集合0, S0, , Sk0, 作為載體，函數(shù)S映射Sk0 Sk10，映射(Sk0, Sl0) Skl0，則得一個(gè)初始代數(shù) 這個(gè)初始代數(shù)和該基調(diào)的標(biāo)準(zhǔn)模型（有后繼算子和加法的自然數(shù)）同構(gòu),2.4 同態(tài)和初始性,初始代數(shù)和其他代數(shù)的比較 1、和有更多元素的代數(shù)比較 多余的元素不能由項(xiàng)定義（有垃圾） 例1：整數(shù)代數(shù)Z 例2：A = Anat, 0A, SA, +A Anat = (0 N) (1 Z) 0A = 0, 0 SAi, n =

28、 i, n +1 i, n +A j, m = max(i, j), n+m,2.4 同態(tài)和初始性,初始代數(shù)和其他代數(shù)的比較 2、和有較少元素的代數(shù)比較 一些不能證明為相等的項(xiàng)在該代數(shù)中被等同（有混淆） 例：模k的自然數(shù),2.4 同態(tài)和初始性,初始代數(shù)的一個(gè)重要特點(diǎn) 初始代數(shù)可能會(huì)滿足不能由E證明的額外的等式 例：自然數(shù)基調(diào)例子中，初始代數(shù)滿足等式 x + y = y + x 因?yàn)?E M = Sk0和E N = Sl0 蘊(yùn)涵 E M + N = Sk+l0 = N + M,2.4 同態(tài)和初始性,自然數(shù)基調(diào)例子中，初始代數(shù)滿足等式 x + y = y + x 不滿足交換律的代數(shù) Anat是所有

29、f : X X的函數(shù)的集合（X至少有兩個(gè)元素） 0A是X上的恒等函數(shù)，SA是Anat上的恒等映射 +A是Anat上的函數(shù)合成 A = Anat 0A SA +A滿足E +A沒有交換性，因?yàn)楹瘮?shù)合成沒有交換性,2.4 同態(tài)和初始性,基項(xiàng)、基代換、基實(shí)例（項(xiàng)、等式） 如果M N 是Termss(, )的項(xiàng)之間的等式，并且S是一個(gè)，基代換，則把SM SN 稱為M N 的基實(shí)例 命題2.18 令E是一組等式，且A對(duì)E來說是初始代數(shù)，則 對(duì)任何等式M N ，下面三個(gè)條件等價(jià) A滿足M N A滿足M N 的每一個(gè)基實(shí)例 M N 的每一個(gè)基實(shí)例都可以從E證明,2.5 代數(shù)數(shù)據(jù)類型,2.5.1 代數(shù)數(shù)據(jù)類型

30、本節(jié)討論數(shù)據(jù)類型公理化方法的一般特征 程序設(shè)計(jì)中的很多數(shù)據(jù)類型 不存在標(biāo)準(zhǔn)的數(shù)學(xué)構(gòu)造，如優(yōu)先隊(duì)列和符號(hào)表 沒有單一和標(biāo)準(zhǔn)的計(jì)算機(jī)實(shí)現(xiàn) 通常是列出它們的操作并公理化地描述這些操作之間的關(guān)系 因此是公理化地定義而不是由數(shù)學(xué)構(gòu)造來定義 困難之處：對(duì)于一個(gè)數(shù)據(jù)類型，難以斷定是否有了“足夠”的公理,2.5 代數(shù)數(shù)據(jù)類型,數(shù)據(jù)抽象的一般原理 抽象數(shù)據(jù)類型由它的規(guī)范定義 使用這樣數(shù)據(jù)類型的程序應(yīng)該只依賴于由它的規(guī)范保證的性質(zhì)，而不依賴于它的任何特定實(shí)現(xiàn) 一個(gè)數(shù)據(jù)類型的函數(shù)可以劃分成 構(gòu)造算子：產(chǎn)生該數(shù)據(jù)類型的一個(gè)新元素 運(yùn)算算子：是該數(shù)據(jù)類型上的函數(shù)，但不產(chǎn)生新的元素 觀察算子：應(yīng)用于該數(shù)據(jù)類型的元素，但返

31、回其它類型的元素，如自然數(shù)或布爾值,2.5 代數(shù)數(shù)據(jù)類型,2.5.2 初始代數(shù)語(yǔ)義和數(shù)據(jù)類型歸納 代數(shù)規(guī)范有幾種不同的“語(yǔ)義”形式 寬松語(yǔ)義：滿足一個(gè)代數(shù)規(guī)范的所有代數(shù)所構(gòu)成的代數(shù)類 初始代數(shù)語(yǔ)義：滿足一個(gè)代數(shù)規(guī)范的所有初始代數(shù)所構(gòu)成的同構(gòu)類 終結(jié)代數(shù)語(yǔ)義：滿足一個(gè)代數(shù)規(guī)范的所有終結(jié)代數(shù)所構(gòu)成的同構(gòu)類 生成語(yǔ)義：滿足一個(gè)代數(shù)規(guī)范的所有生成代數(shù)所構(gòu)成的代數(shù)類,2.5 代數(shù)數(shù)據(jù)類型,初始代數(shù)的性質(zhì) 沒有垃圾 沒有混淆 支持基于數(shù)據(jù)類型構(gòu)造符的歸納 構(gòu)造符集合 Spec , E的函數(shù)符號(hào)集合的子集F0，使得Terms(,)E,的每個(gè)等價(jià)類正好只含一個(gè)由F0的函數(shù)符號(hào)所構(gòu)成的基項(xiàng) 可以基于對(duì)構(gòu)造符的歸

32、納來證明初始代數(shù)的性質(zhì),2.5 代數(shù)數(shù)據(jù)類型,sorts:set, nat, bool 構(gòu)造符、運(yùn)算符、觀察符 fctns:0, 1, 2, : nat+ : nat nat nat Eq? : nat nat booltrue, false bool empty : setinsert : nat set set union : set set setismem? : 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

33、, . . . 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) s = insert y (union s s) condn true x y = x condn false x y = y . . .,2.5 代數(shù)數(shù)據(jù)類型,終結(jié)代數(shù) 在一個(gè)代數(shù)類C中，如果從其中的每個(gè)B到其中某 個(gè)A，都存在

34、唯一的同態(tài)，那么代數(shù)A是終結(jié)代數(shù) 一個(gè)代數(shù)類中的所有終結(jié)代數(shù)都同構(gòu) 若用終結(jié)代數(shù)作為語(yǔ)義，則稱之為終結(jié)語(yǔ)義 如果所有載體都是單元素集合的代數(shù)也在C中，則這個(gè)代數(shù)一定是C的終結(jié)代數(shù),2.5 代數(shù)數(shù)據(jù)類型,初始語(yǔ)義和終結(jié)語(yǔ)義 初始語(yǔ)義：不能證明為相等的就是不相等的 終結(jié)語(yǔ)義：不能證明為不相等的則是相等的 如果把某些類別的解釋固定，而其它類別的解釋用用終結(jié)語(yǔ)義，則它是一個(gè)有用的方法 從初始語(yǔ)義角度看，前面給出的不是集合的規(guī)范,而是表的規(guī)范。因?yàn)椴荒茏C明 insert x(insert y z)=insert y(insert x z) x: nat, y: nat, z: set insert x

35、(insert x z) = insert x zx : nat, z : set 若用終結(jié)語(yǔ)義，且bool的解釋固定,則為集合規(guī)范,2.5 代數(shù)數(shù)據(jù)類型,2.5.3 解釋沒有意義的項(xiàng) 表達(dá)式?jīng)]有意義的情況 除法是一個(gè)部分函數(shù)，除數(shù)為零的表達(dá)式?jīng)]意義 調(diào)用不終止的函數(shù)也構(gòu)成一個(gè)沒有意義的表達(dá)式 如果想在代數(shù)規(guī)范中表示這些情況，必須在基調(diào)中增加表示錯(cuò)誤的項(xiàng)（簡(jiǎn)稱錯(cuò)誤值） 怎樣規(guī)定這些項(xiàng)的值？有三種可能： 什么也不規(guī)定 任意做一個(gè)決定 非常仔細(xì)地說明什么是所需要的,2.6 重寫系統(tǒng),2.6.1 基本定義 重寫系統(tǒng)：用于代數(shù)項(xiàng)的歸約系統(tǒng)R 兩種重要的應(yīng)用 為代數(shù)項(xiàng)提供一種計(jì)算模型 自動(dòng)定理證明 由一

36、組叫做重寫規(guī)則(LR)的有向等式組成 限制：Var(R) Var(L) 由R確定的一步歸約關(guān)系R SLxM R SRxM 關(guān)系R是R的自反傳遞閉包,2.6 重寫系統(tǒng),sorts : nat fctns : 0 : nat : nat nat + : nat nat nat 在這個(gè)基調(diào)上的一些歸約規(guī)則如下： x 0 x x + (x) 0 (x y ) z x + (y + z) 實(shí)例：(x y ) (y) x + (y + (y) x 0 x,2.6 重寫系統(tǒng),引理2.19（歸約保類別） 令R是上的重寫系統(tǒng)，若M Termss(, )且 MRN，則N Termss(, ) 如果N M P蘊(yùn)涵N

37、 P，則關(guān)系（重寫系統(tǒng)）是合流的 若不存在一步歸約的無窮序列M0M1 M2，則關(guān)系（重寫系統(tǒng)）是終止的 不能再歸約的項(xiàng)稱為范式 合流且終止的重寫系統(tǒng)通常又叫做典范系統(tǒng),2.6 重寫系統(tǒng),可變換性 若存在M M1 M2 M3 Mk N，則項(xiàng)M, N Termss(, )是可變換的，寫成 M R N 歸約的無向版本 箭頭的方向并沒有什么意義 對(duì)任何重寫系統(tǒng)，可變換性以及可證明的相等性（把重寫規(guī)則看成等式）是一致的,2.6 重寫系統(tǒng),用自然數(shù)的有窮序列來表示項(xiàng)中的位置 位置n = 1, 2的子項(xiàng)是hab 用M n表示M在位置n的子項(xiàng) 用N nM表示M在n的子項(xiàng)由N代換的結(jié)果 便于引用子項(xiàng)的某個(gè)特定出

38、現(xiàn),2.6 重寫系統(tǒng),2.6.2 合流性和可證明的相等性 記號(hào) 若R是一組重寫規(guī)則，ER用來表示對(duì)應(yīng)的無向的 等式集合 定理2.20 1、對(duì)任何重寫系統(tǒng)R，M RN 當(dāng)且僅當(dāng) ER M N； 2、對(duì)任何合流的重寫系統(tǒng)R，ER M N 當(dāng)且僅當(dāng)M R R N,2.6 重寫系統(tǒng),2.6.3 終止性 良基關(guān)系 集合A上的一個(gè)關(guān)系是良基的，如果不存在A上 元素的無窮遞減序列a0 a1 a2 的話 如果能在項(xiàng)和有良基關(guān)系的集合A的元素間建立起一個(gè)對(duì)應(yīng)，那么可以利用它去證明不存在無窮的歸約序列M0 M1 M2 有幾種方式可把項(xiàng)映射到有良基關(guān)系的集合 1、利用項(xiàng)的語(yǔ)法特點(diǎn) 2、利用代數(shù)的語(yǔ)義結(jié)構(gòu)（下面用這種

39、方式）,2.6 重寫系統(tǒng),代數(shù)A = As1, As2, , f1A, f2A, 是良基的，若 每個(gè)載體As上有一個(gè)良基關(guān)系s 對(duì)每個(gè)n元函數(shù)符號(hào)f，如果x1 y1, , xn yn并且對(duì)某個(gè)i（1 i n）有xi yi，那么 fA(x1, , xn) fA(y1, , yn) 若A是良基代數(shù)，并且M和N都是類別s上的項(xiàng)，若M s N，則寫成 A, M N 如果對(duì)任何環(huán)境都有A, M N，那么寫成A M N,2.6 重寫系統(tǒng),定理2.22 令R是項(xiàng)上的一個(gè)重寫系統(tǒng)，并且令A(yù)是一個(gè) 良基的代數(shù)。如果對(duì)R中每條規(guī)則L R都有 A L R，那么R是終止的 例 x x 載體Abool N 0, 1 (

40、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) 各重寫規(guī)則的左部定義的值都大于其右部定義的值,2.6 重寫系統(tǒng),2.6.4 臨界對(duì) 局部合流 關(guān)系是局部合流的，若N M P 蘊(yùn)涵 N P 局部合流關(guān)系嚴(yán)格弱于合流關(guān)系 例a bb a a a0b b0,2.6 重寫系統(tǒng),cond B (cdr(cons s l) (cons(car l)(cdr l) ) 規(guī)則如下： cdr(cons x l) l cons(car l)(cdr

41、l) l 不相交的歸約,2.6 重寫系統(tǒng),cdr(cons x(cons(car l)(cdr l) 規(guī)則如下： cdr(cons x l) l cons(car l)(cdr l) l 平凡的重迭,2.6 重寫系統(tǒng),cdr(cons(car l)(cdr l) 規(guī)則如下： cdr(cons x l) l cons(car l)(cdr l) l 非平凡的重迭,2.6 重寫系統(tǒng),臨界對(duì) L R cdr(cons x l) l L R cons(car l)(cdr l) l 非平凡重迭是一個(gè)三元組SL，SL，m 二元組SR，SR mSL叫做臨界對(duì) 該例有兩個(gè)臨界對(duì) 第一個(gè)如下： SL是cdr(cons(car l)(cdr l) 臨界對(duì)是cdr l, cdr l,2.6 重寫系統(tǒng),第二個(gè)如下： 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)