Algebraic semantics (computer science)

In computer science, algebraic semantics is a form of axiomatic semantics based on algebraic laws for describing and reasoning about program specifications in a formal manner.^[1][2][3][4]

The syntax of an algebraic specification is formulated in two steps: (1) defining a formal signature of data types and operation symbols, and (2) interpreting the signature through sets and functions.

The signature of an algebraic specification defines its formal syntax. The word "signature" is used like the concept of "key signature" in musical notation.

A signature consists of a set ${\displaystyle S}$ of data types, known as sorts, together with a family ${\displaystyle \Sigma }$ of sets, each set containing operation symbols (or simply symbols) that relate the sorts. We use ${\displaystyle \Sigma _{s_{1}s_{2}...s_{n},~s}}$ to denote the set of operation symbols relating the sorts ${\displaystyle s_{1},~s_{2},~...,~s_{n}\in S}$ to the sort ${\displaystyle s\in S}$.

For example, for the signature of integer stacks, we define two sorts, namely, ${\displaystyle int}$ and ${\displaystyle stack}$, and the following family of operation symbols:

${\displaystyle {\begin{aligned}\Sigma _{\Lambda ,~stack}&=\{{\rm {new}}\}\\\Sigma _{int~stack,~stack}&=\{{\rm {push}}\}\\\Sigma _{stack,~stack}&=\{{\rm {pop}}\}\\\Sigma _{stack,~int}&=\{{\rm {depth}},{\rm {top}}\}\\\end{aligned}}}$

where ${\displaystyle \Lambda }$ denotes the empty string.

An algebra ${\displaystyle A}$ interprets the sorts and operation symbols as sets and functions. Each sort ${\displaystyle s}$ is interpreted as a set ${\displaystyle A_{s}}$, which is called the carrier of ${\displaystyle A}$ of sort ${\displaystyle s}$, and each symbol ${\displaystyle \sigma }$ in ${\displaystyle \Sigma _{s_{1}s_{2}...s_{n},~s}}$ is mapped to a function ${\displaystyle \sigma _{A}:A_{s_{1}}\times A_{s_{2}}\times ~...\times ~A_{s_{n}}}$, which is called an operation of ${\displaystyle A}$.

With respect to the signature of integer stacks, we interpret the sort ${\displaystyle int}$ as the set ${\displaystyle \mathbb {Z} }$ of integers, and interpret the sort ${\displaystyle stack}$