[拼音]：daishu yuyixue

[外文]：algebraic semantics

形式語義學(xué)的一個分支，用代數(shù)方法研究計算機語言的語義。它把計算機語言形式地定義為滿足某種公理體系的抽象代數(shù)結(jié)構(gòu)，然后利用這種代數(shù)結(jié)構(gòu)的性質(zhì)來證明用該語言編寫的程序的正確性。

代數(shù)語義學(xué)始于對抽象數(shù)據(jù)類型的研究。數(shù)據(jù)類型是計算機語言中的重要組成部分。但在60年代中期以前一直缺少科學(xué)的定義。它被認(rèn)為僅僅是一些數(shù)據(jù)的集合，這種觀點不能反映數(shù)據(jù)類型的內(nèi)在數(shù)學(xué)特性，因而不能用來檢驗程序的正確性。1967年問世的SIMULA67語言，第一次提出類程的概念，把數(shù)據(jù)和被允許施行于這些數(shù)據(jù)之上的運算結(jié)合起來，它是現(xiàn)代抽象數(shù)據(jù)類型的開始，但當(dāng)時未引起足夠重視。70年代初，軟件危機促使人們?nèi)パ芯烤帉懞万炞C正確的程序的理論和技術(shù)。在當(dāng)時出現(xiàn)的一些新語言中，進一步把數(shù)據(jù)類型的特性與它的具體表示及實現(xiàn)方式分開來，提高了它的抽象程度。在這種思想指導(dǎo)下，用代數(shù)結(jié)構(gòu)描述數(shù)據(jù)類型的語法，用公理體系描述數(shù)據(jù)類型的語義，就形成了完整的抽象數(shù)據(jù)類型，并出現(xiàn)了研究這種結(jié)構(gòu)的代數(shù)語義學(xué)。

基調(diào)和Σ代數(shù)

用S 表示由一組稱為類子的元素構(gòu)成的集合，用O表示由一組運算符構(gòu)成的集合，則O中每一元素均可表示為：

S₁×S₂×…×S_k─→S_k+1

其中S_i∈S(1≤i≤k+1)，箭頭左邊是運算的變元，右邊是運算的結(jié)果。變元可以為空集，此時它是零元運算符。對偶Σ=(S，O)稱為基調(diào)，它確定數(shù)據(jù)類型的基本語法結(jié)構(gòu)。

給S中的每個類子 S_i賦以一個元素集合A?鄭?給O中的每個k元運算符O_i賦以一個函數(shù)f_i(x₁，x₂，…，x_k)，其中x_j∈A?藎?1≤j≤k，f_i(x₁，x₂，…，x_k)∈A₊₁。令A=｛A?鄭?，F=｛f_i｝，則對偶Σ_A，_F=｛A，F｝稱為以Σ為基調(diào)的一個Σ代數(shù)。A?殖莆?Σ代數(shù)的載體。

Σ代數(shù)是一種非齊性代數(shù)。非齊性代數(shù)是比克霍夫和李普森在1970年作為對以前的齊性代數(shù)的推廣而提出的。在這種代數(shù)里，元素集被分成幾個互不相交的子集。每個代數(shù)運算均以特定的子集為其定義域和值域。非齊性代數(shù)是代數(shù)語義學(xué)的主要工具。

例如，為了定義數(shù)據(jù)類型“整數(shù)堆”，需要三種類子：S₁=bag，S₂=int，S₃=bool和四個運算符

empty：　　 ─→bag

insert：　　bag×integer ─→bag

remove：　　 bag×integer ─→bag

element：　　 bag×integer ─→bool

其中empty是零元運算符，又是載體A_S1中的元素。A_S1=｛empty，…｝，A_S2=｛…，-2，-1，0，1，2，…｝，=｛True，F(xiàn)alse｝。A_S1中的其他元素通過反復(fù)執(zhí)行上述運算而得。

Σ代數(shù)的層次結(jié)構(gòu)

Σ和Σ是兩個具有相同基調(diào)的Σ代數(shù)。如果存在單值映射φ，把A₁映為A₂，F₁映為F₂，且對任意的 ??₁，??₂，…，??_n∈A₁及f₁∈F₁有φ(f₁(??₁，…，??_n))=f₂(φ(??₁)，…，φ(??_n))， 其中f₂∈F₂，φ(f₁)＝f₂。則稱φ為Σ到Σ的一個同態(tài)映射， 如果把它看成態(tài)射，則對應(yīng)于同一基調(diào)的所有Σ代數(shù)構(gòu)成一個范疇。

如果存在一個Σ代數(shù)，表為Σ₁，它屬于以某個Σ為基調(diào)的范疇C，使得對C中的每個Σ代數(shù)Σ_i都存在一個唯一的同態(tài)映射φ_i:Σ₁─→Σ_i，則稱Σ₁為C中的初始代數(shù)。如果存在另一個Σ代數(shù)Σ₂，使得對C中每個Σ_j，都存在一個唯一的同態(tài)映射φ_j:Σ_j─→Σ₂，則稱Σ₂為C 中的終結(jié)代數(shù)。初始代數(shù)和終結(jié)代數(shù)在同構(gòu)意義下都是唯一的。

在上面所說的情況下，這兩種代數(shù)都是存在的。若載體集 A中的任何元素彼此都不等價，即可得初始代數(shù)，又稱項代數(shù)。如果每個類子S_i只對應(yīng)一個元素??_i，即可得終結(jié)代數(shù)。

數(shù)據(jù)類型的語義

對S中的每個類子S_i，取一組自由變量X_i與之對應(yīng)，X=｛X_i｝。設(shè)e_i(x)表示在函數(shù)集F對變量集 X的作用下，所得到的全部屬于類子S_i的表達式集合，e(x)=｛e_i(x)｝，則Σ代數(shù)Σ稱為X上的自由Σ代數(shù)。對任意的i和任意的t₁，t₂∈e_i(x)，公式t₁=t₂稱為一個公理。令 E為由任意一組無矛盾的公理構(gòu)成的集合，對偶｛Σ，E｝稱為一個抽象數(shù)據(jù)類型。

若E⁺為E的閉包，E⁺定義了e(x)上的一個等價關(guān)系。此等價關(guān)系隨賦值X←A而傳遞給載體集A，引導(dǎo)出A上的一個等價關(guān)系。令等價類集為A′，定義對偶｛，E⁺｝為，則也是一個Σ代數(shù)，稱為，的商代數(shù)。所有滿足公理系統(tǒng) E⁺的∑代數(shù)構(gòu)成一個范疇，可以證明商代數(shù) 就是這個范疇中的初始代數(shù)，它被用來定義抽象數(shù)據(jù)類型的語義。初始代數(shù)只是抽象數(shù)據(jù)類型(，E⁺)的一個模型，也有用其他模型，例如終結(jié)代數(shù)，來定義它的語義的。

程序設(shè)計語言的代數(shù)語義

把一個程序設(shè)計語言看成是抽象數(shù)據(jù)類型，就可以用代數(shù)方法來描述它的語義。具體作法是:使每個語法符號對應(yīng)S 中的一個類子，每個語法規(guī)則對應(yīng)O 中的一個運算。又使語義關(guān)系對應(yīng)公理系統(tǒng)E。但這樣做還有一個困難，即上下文條件難以表達。為此要把同態(tài)映射擴充為弱同態(tài)，即允許同態(tài)映射由部分函數(shù)實現(xiàn)。在一定的條件下，弱同態(tài)意義下的終結(jié)代數(shù)是存在的，并等價于程序的最小不動點語義。

建筑資質(zhì)代辦咨詢熱線：13198516101

標(biāo)簽：代數(shù)語義學(xué)

版權(quán)聲明：本文采用知識共享 署名4.0國際許可協(xié)議 [BY-NC-SA] 進行授權(quán)

文章名稱：《代數(shù)語義學(xué)》

文章鏈接：http://m.fjemb.com/14261.html

該作品系作者結(jié)合建筑標(biāo)準(zhǔn)規(guī)范、政府官網(wǎng)及互聯(lián)網(wǎng)相關(guān)知識整合。如若侵權(quán)請通過投訴通道提交信息，我們將按照規(guī)定及時處理。