[拼音]：daishu yuyixue

[外文]：algebraic semantics

形式语义学的一个分支，用代数方法研究计算机语言的语义。它把计算机语言形式地定义为满足某种公理体系的抽象代数结构，然后利用这种代数结构的性质来证明用该语言编写的程序的正确性。

代数语义学始于对抽象数据类型的研究。数据类型是计算机语言中的重要组成部分。但在60年代中期以前一直缺少科学的定义。它被认为仅仅是一些数据的集合，这种观点不能反映数据类型的内在数学特性，因而不能用来检验程序的正确性。1967年问世的SIMULA67语言，第一次提出类程的概念，把数据和被允许施行于这些数据之上的运算结合起来，它是现代抽象数据类型的开始，但当时未引起足够重视。70年代初，软件危机促使人们去研究编写和验证正确的程序的理论和技术。在当时出现的一些新语言中，进一步把数据类型的特性与它的具体表示及实现方式分开来，提高了它的抽象程度。在这种思想指导下，用代数结构描述数据类型的语法，用公理体系描述数据类型的语义，就形成了完整的抽象数据类型，并出现了研究这种结构的代数语义学。

基调和Σ代数

用S 表示由一组称为类子的元素构成的集合，用O表示由一组运算符构成的集合，则O中每一元素均可表示为：

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

其中S_i∈S(1≤i≤k+1)，箭头左边是运算的变元，右边是运算的结果。变元可以为空集，此时它是零元运算符。对偶Σ=(S，O)称为基调，它确定数据类型的基本语法结构。

给S中的每个类子 S_i赋以一个元素集合A捴，给O中的每个k元运算符O_i赋以一个函数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｝称为以Σ为基调的一个Σ代数。A捴称为Σ代数的载体。

Σ代数是一种非齐性代数。非齐性代数是比克霍夫和李普森在1970年作为对以前的齐性代数的推广而提出的。在这种代数里，元素集被分成几个互不相交的子集。每个代数运算均以特定的子集为其定义域和值域。非齐性代数是代数语义学的主要工具。

例如，为了定义数据类型“整数堆”，需要三种类子：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，False｝。A_S1中的其他元素通过反复执行上述运算而得。

Σ代数的层次结构

Σ和Σ是两个具有相同基调的Σ代数。如果存在单值映射φ，把A₁映为A₂，F₁映为F₂，且对任意的 ɑ₁，ɑ₂，…，ɑ_n∈A₁及f₁∈F₁有φ(f₁(ɑ₁，…，ɑ_n))=f₂(φ(ɑ₁)，…，φ(ɑ_n))， 其中f₂∈F₂，φ(f₁)＝f₂。则称φ为Σ到Σ的一个同态映射， 如果把它看成态射，则对应于同一基调的所有Σ代数构成一个范畴。

如果存在一个Σ代数，表为Σ₁，它属于以某个Σ为基调的范畴C，使得对C中的每个Σ代数Σ_i都存在一个唯一的同态映射φ_i:Σ₁─→Σ_i，则称Σ₁为C中的初始代数。如果存在另一个Σ代数Σ₂，使得对C中每个Σ_j，都存在一个唯一的同态映射φ_j:Σ_j─→Σ₂，则称Σ₂为C 中的终结代数。初始代数和终结代数在同构意义下都是唯一的。

在上面所说的情况下，这两种代数都是存在的。若载体集 A中的任何元素彼此都不等价，即可得初始代数，又称项代数。如果每个类子S_i只对应一个元素ɑ_i，即可得终结代数。

数据类型的语义

对S中的每个类子S_i，取一组自由变量X_i与之对应，X=｛X_i｝。设e_i(x)表示在函数集F对变量集 X的作用下，所得到的全部属于类子S_i的表达式集合，e(x)=｛e_i(x)｝，则Σ代数Σ称为X上的自由Σ代数。对任意的i和任意的t₁，t₂∈e_i(x)，公式t₁=t₂称为一个公理。令 E为由任意一组无矛盾的公理构成的集合，对偶｛Σ，E｝称为一个抽象数据类型。

若E⁺为E的闭包，E⁺定义了e(x)上的一个等价关系。此等价关系随赋值X←A而传递给载体集A，引导出A上的一个等价关系。令等价类集为A′，定义对偶｛，E⁺｝为，则也是一个Σ代数，称为，的商代数。所有满足公理系统 E⁺的∑代数构成一个范畴，可以证明商代数 就是这个范畴中的初始代数，它被用来定义抽象数据类型的语义。初始代数只是抽象数据类型(，E⁺)的一个模型，也有用其他模型，例如终结代数，来定义它的语义的。

程序设计语言的代数语义

把一个程序设计语言看成是抽象数据类型，就可以用代数方法来描述它的语义。具体作法是:使每个语法符号对应S 中的一个类子，每个语法规则对应O 中的一个运算。又使语义关系对应公理系统E。但这样做还有一个困难，即上下文条件难以表达。为此要把同态映射扩充为弱同态，即允许同态映射由部分函数实现。在一定的条件下，弱同态意义下的终结代数是存在的，并等价于程序的最小不动点语义。