Algebraic semantics (computer science)

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 S of data types, known as sorts, together with a family \Sigma of sets, each set containing operation symbols (or simply symbols) that relate the sorts. We use \Sigma_{s_1 s_2 ... s_n,~s} to denote the set of operation symbols relating the sorts s_1,~s_2,~...,~s_n \in S to the sort s \in S. For example, for the signature of integer stacks, we define two sorts, namely, int and stack, and the following family of operation symbols: ::\begin{align} \Sigma_{\Lambda,~stack} & = \{ {\rm new} \} \\ \Sigma_{int~stack,~stack} & = \{ {\rm push} \} \\ \Sigma_{stack,~stack} & = \{ {\rm pop} \} \\ \Sigma_{stack,~int} & = \{ {\rm depth}, {\rm top} \} \\ \end{align} where \Lambda denotes the empty string. Set-theoretic interpretation of signature An algebra A interprets the sorts and operation symbols as sets and functions. Each sort s is interpreted as a set A_s, which is called the carrier of A of sort s, and each symbol \sigma in \Sigma_{s_1 s_2 ... s_n,~s} is mapped to a function \sigma_A : A_{s_1} \times A_{s_2} \times~... \times~A_{s_n}, which is called an operation of A. With respect to the signature of integer stacks, we interpret the sort int as the set \Z of integers, and interpret the sort stack as the set Stack of integer stacks. We further interpret the family of operation symbols as the following functions: ::\begin{align} {\rm new} & : ~ \to Stack \\ {\rm push} & : ~ \Z \times Stack \to Stack \\ {\rm pop} & : ~ Stack \to Stack \\ {\rm depth} & : ~ Stack \to \Z \\ {\rm top} & : ~ Stack \to \Z \\ \end{align} ==Semantics==

Semantics refers to the meaning or behavior. An algebraic specification provides both the meaning and behavior of the object in question. Equational axioms The semantics of an algebraic specifications is defined by axioms in the form of conditional equations. of a specification refers to its mathematical meaning. The mathematical semantics of an algebraic specification is the class of all algebras that satisfy the specification. In particular, the classic approach by Goguen et al. of a specification means how to interpret it as a sequence of computational steps. We define a ground term as an algebraic expression without variables. The operational semantics of an algebraic specification refers to how ground terms can be transformed using the given equational axioms as left-to-right rewrite rules, until such terms reach their normal forms, where no more rewriting is possible. Consider the axioms for integer stacks. Let "\Rrightarrow" denote "rewrites to". ::\begin{align} & {\rm top} ({\rm pop} ({\rm pop} ({\rm push} (1,~{\rm push} (2,~{\rm push} (3,~{\rm pop} ({\rm new}))))))) & \\ \Rrightarrow ~ & {\rm top} ({\rm pop} ({\rm pop} ({\rm push} (1,~{\rm push} (2,~{\rm push} (3,~{\rm new})))))) & ({\rm by~Axiom~} A4) \\ \Rrightarrow ~ & {\rm top} ({\rm pop} ({\rm push} (2,~{\rm push} (3,~{\rm new})))) & ({\rm by~Axiom~} A1) \\ \Rrightarrow ~ & {\rm top} ({\rm push} (3,~{\rm new})) & ({\rm by~Axiom~} A1) \\ \Rrightarrow ~ & 3 & ({\rm by~Axiom~} A3) \\ \end{align} Canonical property An algebraic specification is said to be confluent (also known as Church-Rosser) if the rewriting of any ground term leads to the same normal form. It is said to be terminating if the rewriting of any ground term will lead to a normal form after a finite number of steps. The algebraic specification is said to be canonical (also known as convergent) if it is both confluent and terminating. In other words, it is canonical if the rewriting of any ground term leads to a unique normal form after a finite number of steps. Given any canonical algebraic specification, the mathematical semantics agrees with the operational semantics. As a result, canonical algebraic specifications have been widely applied to address program correctness issues. For example, numerous researchers have applied such specifications to the testing of observational equivalence of objects in object-oriented programming. See Chen and Tse as a secondary source that provides a historical review of prominent research from 1981 to 2013. == See also ==