代數語義學

代數語義學

代數語義學是形式語義學的一個分支,用代數方法研究計算機語言的語義。

代數語義學


形式語義學的一個分支,用代數方法研究計算機語言的語義。它把計算機語言形式地定義為滿足某種公理體系的抽象代數結構,然後利用這種代數結構的性質來證明用該語言編寫的程序的正確性。
代數語義學始於對抽象數據類型的研究。數據類型是計算機語言中的重要組成部分。但在60年代中期以前一直缺少科學的定義。它被認為僅僅是一些數據的集合,這種觀點不能反映數據類型的內在數學特性,因而不能用來檢驗程序的正確性。1967年問世的SIMULA67語言,第一次提出類程的概念,把數據和被允許施行於這些數據之上的運算結合起來,它是現代抽象數據類型的開始,但當時未引起足夠重視。70年代初,軟體危機促使人們去研究編寫和驗證正確的程序的理論和技術。在當時出現的一些新語言中,進一步把數據類型的特性與它的具體表示及實現方式分開來,提高了它的抽象程度。在這種思想指導下,用代數結構描述數據類型的語法,用公理體系描述數據類型的語義,就形成了完整的抽象數據類型,並出現了研究這種結構的代數語義學。
基調和Σ代數 用S 表示由一組稱為類子的元素構成的集合,用O表示由一組運算符構成的集合,則O中每一元素均可表示為:
S1×S2×…×Sk─→Sk+1
其中Si∈S(1≤i≤k+1),箭頭左邊是運算的變元,右邊是運算的結果。變元可以為空集,此時它是零元運算符。對偶Σ=(S,O)稱為基調,它確定數據類型的基本語法結構。
給S中的每個類子 Si賦以一個元素集合A捴,給O中的每個k元運算符Oi賦以一個函數fi(x1,x2,…,xk),其中xj∈A捿,1≤j≤k,fi(x1,x2,…,xk)∈A
代數語義學
代數語義學
+1。令A={A捴},F={fi},則對偶ΣA,F={A,F}稱為以Σ為基調的一個Σ代數。A捴稱為Σ代數的載體。
Σ代數是一種非齊性代數。非齊性代數是比克霍夫和李普森在1970年作為對以前的齊性代數的推廣而提出的。在這種代數里,元素集被分成幾個互不相交的子集。每個代數運算均以特定的子集為其定義域和值域。非齊性代數是代數語義學的主要工具。
例如,為了定義數據類型“整數堆”,需要三種類子:S1=bag,S2=int,S3=bool和四個運算符
empty: ─→bag
insert: bag×integer ─→bag
remove: bag×integer ─→bag
element: bag×integer ─→bool
其中empty是零元運算符,又是載體AS1中的元素。AS1={empty,…},AS2={…,-2,-1,0,1,2,…},
代數語義學
代數語義學
={True,False}。AS1中的其他元素通過反覆執行上述運算而得。
Σ代數的層次結構 Σ
代數語義學
代數語義學
和Σ
代數語義學
代數語義學
是兩個具有相同基調的Σ代數。如果存在單值映射φ,把A1映為A2,F1映為F2,且對任意的 ɑ1,ɑ2,…,ɑn∈A1及f1∈F1有φ(f1(ɑ1,…,ɑn))=f2(φ(ɑ1),…,φ(ɑn)), 其中f2∈F2,φ(f1)=f2。則稱φ為Σ
代數語義學
代數語義學
到Σ
代數語義學
代數語義學
的一個同態映射, 如果把它看成態射,則對應於同一基調的所有Σ代數構成一個範疇。
如果存在一個Σ代數,表為Σ1,它屬於以某個Σ為基調的範疇C,使得對C中的每個Σ代數Σi都存在一個唯一的同態映射φi:Σ1─→Σi,則稱Σ1為C中的初始代數。如果存在另一個Σ代數Σ2,使得對C中每個Σj,都存在一個唯一的同態映射φj:Σj─→Σ2,則稱Σ2為C 中的終結代數。初始代數和終結代數在同構意義下都是唯一的。
在上面所說的情況下,這兩種代數都是存在的。若載體集 A中的任何元素彼此都不等價,即可得初始代數,又稱項代數。如果每個類子Si只對應一個元素ɑi,即可得終結代數。
數據類型的語義 對S中的每個類子Si,取一組自由變數Xi與之對應,X={Xi}。設ei(x)表示在函數集F對變數集 X的作用下,所得到的全部屬於類子Si的表達式集合,e(x)={ei(x)},則Σ代數Σ
代數語義學
代數語義學
稱為X上的自由Σ代數。對任意的i和任意的t1,t2∈ei(x),公式t1=t2稱為一個公理。令 E為由任意一組無矛盾的公理構成的集合,對偶{Σ,E}稱為一個抽象數據類型。
若E+為E的閉包,E+定義了e(x)上的一個等價關係。此等價關係隨賦值X←A而傳遞給載體集A,引導出A上的一個等價關係。令等價類集為A′,定義對偶
代數語義學
代數語義學
,E+}為
代數語義學
代數語義學
,則
代數語義學
代數語義學
也是一個Σ代數,稱為,
代數語義學
代數語義學
的商代數。所有滿足公理系統 E+的∑代數
代數語義學
代數語義學
構成一個範疇,可以證明商代數
代數語義學
代數語義學
就是這個範疇中的初始代數,它被用來定義抽象數據類型的語義。初始代數只是抽象數據類型(
代數語義學
代數語義學
,E+)的一個模型,也有用其他模型,例如終結代數,來定義它的語義的。
程序設計語言的代數語義 把一個程序設計語言看成是抽象數據類型,就可以用代數方法來描述它的語義。具體作法是:使每個語法符號對應S 中的一個類子,每個語法規則對應O 中的一個運算。又使語義關係對應公理系統E。但這樣做還有一個困難,即上下文條件難以表達。為此要把同態映射擴充為弱同態,即允許同態映射由部分函數實現。在一定的條件下,弱同態意義下的終結代數是存在的,並等價於程序的最小不動點語義。