Algebraic semantics (computer science)

Last updated September 30, 2023

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 $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{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 $\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 $\mathbb {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{aligned}{\rm {new}}&:~\to Stack\\{\rm {push}}&:~\mathbb {Z} \times Stack\to Stack\\{\rm {pop}}&:~Stack\to Stack\\{\rm {depth}}&:~Stack\to \mathbb {Z} \\{\rm {top}}&:~Stack\to \mathbb {Z} \\\end{aligned}}

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.^[1]

With respect to the signature of integer stacks, we have the following axioms:

For any

z\in \mathbb {Z}

and

s\in Stack

,

{\begin{aligned}&A1:~~{\rm {pop}}({\rm {push}}(z,s))=s\\&A2:~~{\rm {depth}}({\rm {push}}(z,s))={\rm {depth}}(s)+1\\&A3:~~{\rm {top}}({\rm {push}}(z,s))=z\\&A4:~~{\rm {pop}}({\rm {new}})={\rm {new}}\\&A5:~~{\rm {depth}}({\rm {new}})=0\\&A6:~~{\rm {top}}(s)=-404~{\rm {if~depth}}(s)=0\\\end{aligned}}

where "

-404

" indicates "not found".

Mathematical semantics

The mathematical semantics (also known as denotational semantics)^[5] 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.^[1]^[2] takes the initial algebra (unique up to isomorphism) as the "most representative" model of the algebraic specification.

Operational semantics

The operational semantics ^[6] 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{aligned}&{\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{aligned}}

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.^[7]

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^[8] as a secondary source that provides a historical review of prominent research from 1981 to 2013.

Related Research Articles

In mathematics, an associative algebraA is an algebraic structure with compatible operations of addition, multiplication, and a scalar multiplication by elements in some field K. The addition and multiplication operations together give A the structure of a ring; the addition and scalar multiplication operations together give A the structure of a vector space over K. In this article we will also use the term K-algebra to mean an associative algebra over the field K. A standard first example of a K-algebra is a ring of square matrices over a field K, with the usual matrix multiplication.

In mathematical physics and mathematics, the Pauli matrices are a set of three $2 \times 2$ complex matrices which are Hermitian, involutory and unitary. Usually indicated by the Greek letter sigma, they are occasionally denoted by tau when used in connection with isospin symmetries.

<span class="mw-page-title-main">Singular value decomposition</span> Matrix decomposition

In linear algebra, the singular value decomposition (SVD) is a factorization of a real or complex matrix. It generalizes the eigendecomposition of a square normal matrix with an orthonormal eigenbasis to any $matrix. It is related to the polar decomposition.$

In mathematics, the unitary group of degree n, denoted U(n), is the group of n × n unitary matrices, with the group operation of matrix multiplication. The unitary group is a subgroup of the general linear group GL(n, C). Hyperorthogonal group is an archaic name for the unitary group, especially over finite fields. For the group of unitary matrices with determinant 1, see Special unitary group.

In mathematics, in particular in algebraic topology, differential geometry and algebraic geometry, the Chern classes are characteristic classes associated with complex vector bundles. They have since become fundamental concepts in many branches of mathematics and physics, such as string theory, Chern–Simons theory, knot theory, Gromov–Witten invariants.

In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems. In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.

In algebraic topology, singular homology refers to the study of a certain set of algebraic invariants of a topological space X, the so-called homology groups $Intuitively, singular homology counts, for each dimension n, the n -dimensional holes of a space. Singular homology is a particular example of a homology theory, which has now grown to be a rather broad collection of theories. Of the various theories, it is perhaps one of the simpler ones to understand, being built on fairly concrete constructions.$

In mathematics, a gerbe is a construct in homological algebra and topology. Gerbes were introduced by Jean Giraud following ideas of Alexandre Grothendieck as a tool for non-commutative cohomology in degree 2. They can be seen as an analogue of fibre bundles where the fibre is the classifying stack of a group. Gerbes provide a convenient, if highly abstract, language for dealing with many types of deformation questions especially in modern algebraic geometry. In addition, special cases of gerbes have been used more recently in differential topology and differential geometry to give alternative descriptions to certain cohomology classes and additional structures attached to them.

In algebraic topology, a branch of mathematics, a spectrum is an object representing a generalized cohomology theory. Every such cohomology theory is representable, as follows from Brown's representability theorem. This means that, given a cohomology theory

$,$

The notion of institution was created by Joseph Goguen and Rod Burstall in the late 1970s, in order to deal with the "population explosion among the logical systems used in computer science". The notion attempts to "formalize the informal" concept of logical system.

String diagrams are a formal graphical language for representing morphisms in monoidal categories, or more generally 2-cells in 2-categories. They are a prominent tool in applied category theory. When interpreted in the monoidal category of vector spaces and linear maps with the tensor product, string diagrams are called tensor networks or Penrose graphical notation. This has led to the development of categorical quantum mechanics where the axioms of quantum theory are expressed in the language of monoidal categories.

In universal algebra and in model theory, a structure consists of a set along with a collection of finitary operations and relations that are defined on it.

Indexed grammars are a generalization of context-free grammars in that nonterminals are equipped with lists of flags, or index symbols. The language produced by an indexed grammar is called an indexed language.

In formal language theory, a grammar describes how to form strings from a language's alphabet that are valid according to the language's syntax. A grammar does not describe the meaning of the strings or what can be done with them in whatever context—only their form. A formal grammar is defined as a set of production rules for such strings in a formal language.

In physics, and specifically in quantum field theory, a bispinor is a mathematical construction that is used to describe some of the fundamental particles of nature, including quarks and electrons. It is a specific embodiment of a spinor, specifically constructed so that it is consistent with the requirements of special relativity. Bispinors transform in a certain "spinorial" fashion under the action of the Lorentz group, which describes the symmetries of Minkowski spacetime. They occur in the relativistic spin-1/2 wave function solutions to the Dirac equation.

In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact.

The Vanna–Volga method is a mathematical tool used in finance. It is a technique for pricing first-generation exotic options in foreign exchange market (FX) derivatives.

In physics, particularly in quantum field theory, the Weyl equation is a relativistic wave equation for describing massless spin-1/2 particles called Weyl fermions. The equation is named after Hermann Weyl. The Weyl fermions are one of the three possible types of elementary fermions, the other two being the Dirac and the Majorana fermions.

In mathematical physics, the Gordon decomposition of the Dirac current is a splitting of the charge or particle-number current into a part that arises from the motion of the center of mass of the particles and a part that arises from gradients of the spin density. It makes explicit use of the Dirac equation and so it applies only to "on-shell" solutions of the Dirac equation.

References

1 2 3 J.A. Goguen; J.W. Thatcher; E.G. Wagner; J.B. Wright (1977). "Initial algebra semantics and continuous algebras". Journal of the ACM . 24 (1): 68–95. doi: 10.1145/321992.321997 . S2CID 11060837.
1 2 J.A. Goguen; J.W. Thatcher; E.G. Wagner (1978). "An initial algebra approach to the specification, correctness and implementation of abstract data types". In R.T. Yeh (ed.). Current Trends in Programming Methodology, Vol. IV: Data Structuring. Prentice Hall. pp. 80–149.
↑ J.A. Goguen; C. Kirchner; H. Kirchner; A. Megrelis; J. Meseguer (1988). "An introduction to OBJ3". Proceedings of the First Workshop on Conditional Term Rewriting Systems. Lecture Notes in Computer Science. Vol. 308. Springer. pp. 258–263. doi:10.1007/3-540-19242-5_22. ISBN 978-3-540-19242-8.
↑ J.A. Goguen; G. Malcolm (1996). Algebraic Semantics of Imperative Programs. MIT Press. ISBN 9780262071727.
↑ David A. Schmidt (1986). Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers. ISBN 9780205104505.
↑ Gordon D. Plotkin (1981). "A structural approach to operational semantics" (Technical Report DAIMI FN-19). Computer Science Department, Aarhus University.
↑ S. Lucas; J. Meseguer (2014). "Strong and Weak Operational Termination of Order-Sorted Rewrite Theories". In S. Escobar (ed.). Rewriting Logic and Its Applications. Lecture Notes in Computer Science. Vol. 8663. Cham: Springer. pp. 178–194. doi:10.1007/978-3-319-12904-4_10. ISBN 978-3-319-12903-7.
↑ H.Y. Chen; T.H. Tse (2013). "Equality to equals and unequals: A revisit of the equivalence and nonequivalence criteria in class-level testing of object-oriented software". IEEE Transactions on Software Engineering . 39 (11): 1549–1563. doi:10.1109/TSE.2013.33. hdl: 10722/187124 . S2CID 8694513.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[goguen1977-1] 1 2 3 J.A. Goguen; J.W. Thatcher; E.G. Wagner; J.B. Wright (1977). "Initial algebra semantics and continuous algebras". Journal of the ACM . 24 (1): 68–95. doi: 10.1145/321992.321997 . S2CID 11060837.

[goguen1978-2] 1 2 J.A. Goguen; J.W. Thatcher; E.G. Wagner (1978). "An initial algebra approach to the specification, correctness and implementation of abstract data types". In R.T. Yeh (ed.). Current Trends in Programming Methodology, Vol. IV: Data Structuring. Prentice Hall. pp. 80–149.

[3] J.A. Goguen; C. Kirchner; H. Kirchner; A. Megrelis; J. Meseguer (1988). "An introduction to OBJ3". Proceedings of the First Workshop on Conditional Term Rewriting Systems. Lecture Notes in Computer Science. Vol. 308. Springer. pp. 258–263. doi:10.1007/3-540-19242-5_22. ISBN 978-3-540-19242-8.

[4] J.A. Goguen; G. Malcolm (1996). Algebraic Semantics of Imperative Programs. MIT Press. ISBN 9780262071727.

[5] David A. Schmidt (1986). Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers. ISBN 9780205104505.

[6] Gordon D. Plotkin (1981). "A structural approach to operational semantics" (Technical Report DAIMI FN-19). Computer Science Department, Aarhus University.

[7] S. Lucas; J. Meseguer (2014). "Strong and Weak Operational Termination of Order-Sorted Rewrite Theories". In S. Escobar (ed.). Rewriting Logic and Its Applications. Lecture Notes in Computer Science. Vol. 8663. Cham: Springer. pp. 178–194. doi:10.1007/978-3-319-12904-4_10. ISBN 978-3-319-12903-7.

[8] H.Y. Chen; T.H. Tse (2013). "Equality to equals and unequals: A revisit of the equivalence and nonequivalence criteria in class-level testing of object-oriented software". IEEE Transactions on Software Engineering . 39 (11): 1549–1563. doi:10.1109/TSE.2013.33. hdl: 10722/187124 . S2CID 8694513.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]