代數語義學

形式語義學的一個分支，用代數方法研究計算機語言的語義。它把計算機語言形式地定義為滿足某種公理體系的抽象代數結構，然後利用這種代數結構的性質來證明用該語言編寫的程序的正確性。

代數語義學始於對抽象數據類型的研究。數據類型是計算機語言中的重要組成部分。但在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。但這樣做還有一個困難,即上下文條件難以表達。為此要把同態映射擴充為弱同態，即允許同態映射由部分函數實現。在一定的條件下，弱同態意義下的終結代數是存在的，並等價於程序的最小不動點語義。