【正文】 specification TRUTH_VALUE_LISTS include instantiation of LISTS by TRUTH_VALUES using Truth_Value for Component renamed using Truth_Value_List for List end specification (2) 操作參數(shù)化 specification ARRAYS include NATURALS formal sort Component formal operation maxsize: Natural sort Array operations empty_array : Array modify(_,_,_): Natural , Component , Array→Array ponent_of: Natural , Array→Component variables c : Component j , j : Natural a : Array equations ponent i of modify(j , c , a) = c if i is j ∧ i maxsize () ponent i of modify(j , c , a) = ponent i of a if not (i is j) () modify(i , c , a) = a if not (imaxsize) () end specification 作為實(shí)例化的一個例子 ， 請看以下的最大長度為 6的真假值數(shù)組的規(guī)格說明 : specification TRUTH_VALUE ARRAYS include instantiation of ARRAYS by TRUTH_VALUES using Truth_Value of Component succ succ succ succ succ succ 0 for maxsize renamed using Truth_Value_Array for Array end specification λ演算的代數(shù)規(guī)格說明 λ演算的 α， β， η三種歸約。如果我們定義一個置換函數(shù) sub(M , a , b)表示 a在表達(dá)式 M中所有自由出現(xiàn)均以 b置換，則三種歸約描述為 : α if w is not free in M then (λu . M) = (λw . sub(M , u , w)) β ((λx . M)N) = sub (M , x , N) η if x is not free in M then (λx . (Mx)) = M specification LAMBDA_CLACULUS include TRUTH_VALUES sorts Expr , 1d operations firstid: 1d nextid_ : 1d → 1d equals(_,_): 1d , 1d → Truth_Value var_ : 1d → Expr ap(_,_): Expr , Expr→Expr abs(_,_): 1d , Expr → Expr * sub (_,_,_): Expr , 1d , Expr→Expr * notfree(_,_): 1d , Expr→Truth_Value variables v , w , x , y: 1d M , N , E: Expr equations equals(x , x) = true equals(firstid , next(x)) = false equals(nextid(x) , firstid) = false equals(nextid(x) , nextid(y)) = equals(x,y) notfree(x,var(y) = not equals(x,y) notfree(x , app(M , N)) = notfree(x , M) ∧ notfree(x , N) notfree(x , abs(y , M)) = equals(x , y) ∨ not free(x , M) abs (v , M) = if notfree(w , M) then abs(w , sub(M , v , var(w)) else abs(v , M) //α 歸約 app (abs( , x , M) , N) = sub(M , x , N) //β歸約 abs(x , (app(M , var(x))) = if notfree(x , M) then M else abs(x , app(M , var(x))) // η歸約 sub(var(y) , x , E) = if equals(x , y) then E else var(y) sub(app(M , N) , x , E) = app(sub(M , x , E) , sub (N , x , E)) sub(abs(y , M) , x , E) = if equals(x , y) then abs(y , M) else if notfree(y , E) then abs(y , sub(M , x , E)) else sub(abs(y , M) , x , E) end specification ? 小結(jié) ? 本章我們介紹了代數(shù)語義學(xué) ， 目標(biāo)是以代數(shù)理論建立描述程序規(guī)格說明的代數(shù)模型 ， 并介紹具體的定義方法 。 ? 代數(shù)按不同的抽象層次有具體代數(shù) (定義值集 ， 操作集 )、 抽象代數(shù)(值和操作關(guān)系 )和泛代數(shù) (代數(shù)間關(guān)系 )。 ? 代數(shù)間關(guān)系最重要是同態(tài)映射 ， 同構(gòu)是兩代數(shù)有對等的同態(tài)映射 。 ? 交換圖可清晰描述范疇中代數(shù)對象的映射關(guān)系 。 ? ∑_代數(shù)是給定型構(gòu) ∑上的代數(shù) 。 ∑_同態(tài) 、 同構(gòu)指項(xiàng)代數(shù)上的 。 ? 給定一 ∑必然得到一類代數(shù) ， 初始代數(shù)即對代數(shù)類中每一 ∑_代數(shù)都有唯一 ∑同態(tài)的代數(shù) 。 ? 初始代數(shù)就符號意義是不重復(fù)的 ， 但其實(shí)際值可能相同 ， 因此引出全等類概念 。 ∑_全等工具是說 ∑代數(shù)的承載子有等價關(guān)系 R， 按 R歸類即得全等類 。 ? 按全等的等價關(guān)系 R歸類過程稱商化 ， 商化結(jié)果得的值集構(gòu)成商代數(shù) ， 商代數(shù)可以看作是簡化了的字代數(shù) ， 并包含全等概念 。 ? 泛同構(gòu)映射指商代數(shù)尋求同構(gòu)的映射 。 ? Sp_代數(shù)可以是字代數(shù)上某個全等關(guān)系 ， 或字代數(shù)上某個商代數(shù)描述 。目的是前者 ， 以等式集合給出全等類的公理定義 。