Algebraic semantics (computer science): Difference between revisions

Content deleted Content added

Inline

Revision as of 10:13, 6 December 2021

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 phrase "key signature" in music.

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.

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) 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 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.

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

References

^ ^a ^b 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.
^ ^a ^b 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. Springer. pp. 258–263. doi:10.1007/3-540-19242-5_22.
^ J.A. Goguen; G. Malcolm (1996). Algebraic semantics of imperative programs. MIT Press. ISBN 9780262071727.
^ 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.

@@ Line 3: / Line 3: @@
 -->
 {{Semantics}}
-In [[computer science]], '''algebraic semantics''' is a form of [[axiomatic semantics]] based on [[algebra]]ic laws for describing and reasoning about [[program specification]]s in a [[formal methods|formal]] manner.<ref name=goguen1978> {{cite book |author1=J.A. Goguen |author-link=Joseph Goguen |author2=J.W. Thatcher| author3=E.G. Wagner |chapter=An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types |title=Current Trends in Programming Methodology, Vol. IV: Data Structuring |editor=R.T. Yeh |pages=80-149 |publisher=Prentice Hall | date=1978}}</ref><ref>{{cite book |author1=J.A. Goguen |author-link=Joseph Goguen |author2=C. Kirchner |author3=H. Kirchner |author4=A. Megrelis |author5=J. Meseguer |chapter=An Introduction to OBJ3 |title=Proceedings of the First Workshop on Conditional Term Rewriting Systems |pages=258-263 |publisher=Springer |date=1988}}</ref><ref> {{cite book|author1=J.A. Goguen |author-link=Joseph Goguen |author2=G. Malcolm|title=Algebraic semantics of imperative programs|year=1996|publisher=MIT Press|isbn=9780262071727}}</ref>
+In [[computer science]], '''algebraic semantics''' is a form of [[axiomatic semantics]] based on [[algebra]]ic laws for describing and [[Reason|reasoning]] about [[program specification]]s in a [[formal methods|formal]] manner.
+<ref name=goguen1977> {{cite journal |title=Initial algebra semantics and continuous algebras |author1=J.A. Goguen |author2=J.W. Thatcher |author3=E.G. Wagner |author4=J.B. Wright |journal=[[Journal of the ACM]] |volume=24 |issue=1 |date=1977 |pages=68–95 |url=https://dl.acm.org/doi/abs/10.1145/321992.321997 |doi=10.1145/321992.321997}}</ref><ref name=goguen1978> {{cite book |author1=J.A. Goguen |author-link=Joseph Goguen |author2=J.W. Thatcher| author3=E.G. Wagner |chapter=An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types |title=Current Trends in Programming Methodology, Vol. IV: Data Structuring |editor=R.T. Yeh |pages=80-149 |publisher=[[Prentice Hall]] | date=1978}}</ref><ref>{{cite book |author1=J.A. Goguen |author-link=Joseph Goguen |author2=C. Kirchner |author3=H. Kirchner |author4=A. Megrelis |author5=J. Meseguer |chapter=An Introduction to OBJ3 |title=Proceedings of the First Workshop on Conditional Term Rewriting Systems |pages=258-263 |publisher=[[Springer Science+Business Media|Springer]] |date=1988 |chapter-url=https://link.springer.com/chapter/10.1007/3-540-19242-5_22 |doi=10.1007/3-540-19242-5_22}}</ref><ref> {{cite book|author1=J.A. Goguen |author-link=Joseph Goguen |author2=G. Malcolm|title=Algebraic semantics of imperative programs|year=1996|publisher=[[MIT Press]]|isbn=9780262071727 |url=https://mitpress.mit.edu/books/algebraic-semantics-imperative-programs}}</ref>
 <!--
 <ref>{{cite book|editor1=Samson Abramsky |editor2=Dov M. Gabbay |editor3=Thomas S. E. Maibaum |title=Handbook of Logic in Computer Science|year=1995|volume=Vol. 3: Semantic structures|publisher=Clarendon Press|isbn=9780198537625|author=Eric G. Wagner|chapter=Algebraic Semantics|pages=323–393}}</ref>
@@ Line 9: / Line 11: @@
 ==Syntax==
-The [[Syntax (programming languages)|syntax]] of an [[algebraic specification]] is formulated in two steps: (1) defining a signature of data types and operation symbols, and (2) interpreting the signature through sets and functions.
+The [[Syntax (programming languages)|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 (logic)|signature]] of an algebraic specification defines its formal syntax. The word "signature" is used like the phrase "[[key signature]]" in music.
+A signature consists of a [[Set (mathematics)|set]] <math>S</math> of [[data type]]s, known as [[Many-sorted logic|sorts]], together with a [[Family of sets|family]] <math>\Sigma</math> of sets, each set containing [[Symbol|operation symbols]] (or simply symbols) that relate the sorts.
-===Definition of a Signature===
-A [[Signature (logic)|signature]] consists of a [[Set (mathematics)|set]] <math>S</math> of [[data type]]s, known as [[Many-sorted logic|sorts]], together with a [[Family of sets|family]] <math>\Sigma</math> of sets, each set containing [[Symbol|operation symbols]] (or simply symbols) that relate the sorts.
 We use <math>\Sigma_{s_1 s_2 ... s_n,~s}</math> to denote the set of operation symbols relating the sorts <math>s_1,~s_2,~...,~s_n \in S</math> to the sort <math>s \in S</math>.
@@ Line 24: / Line 28: @@
 where <math>\Lambda</math> denotes the [[empty string]].
-===Set-theoretic interpretation of the signature===
+===Set-theoretic interpretation of signature===
-An [[Universal algebra|algebra]] <math>A</math> interprets the sorts and operation symbols as families of sets and [[Function (mathematics)|functions]].
+An [[Universal algebra|algebra]] <math>A</math> interprets the sorts and operation symbols as sets and [[Function (mathematics)|functions]].
 Each sort <math>s</math> is interpreted as a set <math>A_s</math>, which is called the carrier of <math>A</math> of sort <math>s</math>, and each symbol <math>\sigma</math> in <math>\Sigma_{s_1 s_2 ... s_n,~s}</math> is mapped to a function <math>\sigma_A : A_{s_1} \times A_{s_2} \times~... \times~A_{s_n}</math>, which is called an [[Operation (mathematics)|operation]] of <math>A</math>.
@@ Line 63: / Line 67: @@
 The mathematical semantics of an algebraic specification is the [[Class (set theory)|class]] of all algebras that satisfy the specification.
-In particular, the classic approach by Goguen et al.<ref name=goguen1978/> takes the [[initial algebra]] ([[Uniqueness quantification|unique]] up to [[isomorphism]]) as the "most representative" model of the algebraic specification.
+In particular, the classic approach by Goguen et al.<ref name=goguen1977/><ref name=goguen1978/> takes the [[initial algebra]] ([[Uniqueness quantification|unique]] up to [[isomorphism]]) as the "most representative" model of the algebraic specification.
 ===Operational semantics===
@@ Line 95: / Line 99: @@
 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 [[Software testing|testing]] of [[observational equivalence]] of [[Object (computer science)|objects]] in [[object-oriented programming]]. See Chen and Tse<ref>{{cite journal |last1=H.Y. Chen |last2=T.H. Tse |title=Equality to equals and unequals: A revisit of the equivalence and nonequivalence criteria in class-level testing of object-oriented software |journal=[[IEEE Transactions on Software Engineering]] |volume=39 |issue=11 |pages=1549-1563 |date=2013 |url=https://doi.org/10.1109/TSE.2013.33 |doi=10.1109/TSE.2013.33 |hdl=10722/187124 |hdl-access=free }}</ref> as a [[secondary source]] for the prominent research from 1981 to 2013.
+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 [[Software testing|testing]] of [[observational equivalence]] of [[Object (computer science)|objects]] in [[object-oriented programming]]. See Chen and Tse<ref>{{cite journal |last1=H.Y. Chen |last2=T.H. Tse |title=Equality to equals and unequals: A revisit of the equivalence and nonequivalence criteria in class-level testing of object-oriented software |journal=[[IEEE Transactions on Software Engineering]] |volume=39 |issue=11 |pages=1549-1563 |date=2013 |url=https://doi.org/10.1109/TSE.2013.33 |doi=10.1109/TSE.2013.33 |hdl=10722/187124 |hdl-access=free }}</ref> as a [[secondary source]] that provides a historical review of prominent research from 1981 to 2013.
 == References ==