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]

Syntax

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.

Definition of a signature

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.

Set-theoretic interpretation of signature

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}$