View source for Semantics (computer science)

{{confuse|Computational semantics}}
{{Short description|Mathematical study of the meaning of programming languages}}
{{Semantics}}
{{Formal languages}}

In [[programming language theory]], '''semantics''' is the rigorous mathematical logic study of the meaning of [[programming language]]s.<ref>{{cite book |author-link=Joseph Goguen|first=Joseph A.|last=Goguen |chapter=Semantics of computation |title=Category Theory Applied to Computation and Control |series=Lecture Notes in Computer Science |publisher=[[Springer Publishing|Springer]] |date=1975 |volume=25 |pages=151–163 |doi=10.1007/3-540-07142-3_75|isbn=978-3-540-07142-6 }}</ref> Semantics assigns [[computation]]al meaning to valid [[string (computer science)|strings]] in a [[programming language syntax]]. It is closely related to, and often crosses over with, the [[Semantics of logic|semantics of mathematical proofs]].

'''Semantics''' describes the processes a computer follows when [[Execution (computing)|executing]] a program in that specific language. This can be done by describing the relationship between the input and output of a program, or giving an explanation of how the program will be executed on a certain [[computer platform|platform]], thereby creating a [[model of computation]].

==History==

In 1967, [[Robert W. Floyd]] published the paper ''Assigning meanings to programs''; his chief aim was "a rigorous standard for proofs about computer programs, including [[formal verification|proofs of correctness]], equivalence, and termination".<ref name=floyd>{{cite book |year=1967 |author-link=Robert W. Floyd |first=Robert W. |last=Floyd |chapter=Assigning Meanings to Programs |chapter-url=https://people.eecs.berkeley.edu/~necula/Papers/FloydMeaning.pdf |editor-first=J.T. |editor-last=Schwartz |title=Mathematical Aspects of Computer Science |publisher=American Mathematical Society |isbn=0821867288 |pages=19–32 |url=https://books.google.com/books?id=ynigSICJflYC |series=Proceedings of Symposium on Applied Mathematics |volume=19 }}</ref><ref>{{cite web |author-link=Donald Knuth|author-first=Donald E.|author-last=Knuth |title=Memorial Resolution: Robert W. Floyd (1936–2001) |url=https://stacks.stanford.edu/file/druid:zy788sr3998/SC0193_MemorialResolution_Floyd_Robert.pdf |work=Stanford University Faculty Memorials |publisher=Stanford Historical Society }}</ref> Floyd further wrote:{{r|floyd}}
<blockquote>
A semantic definition of a programming language, in our approach, is founded on a [[Syntax (programming languages)|syntactic]] definition. It must specify which of the phrases in a syntactically correct program represent [[Command (computing)|commands]], and what [[Conditional (computer programming)|conditions]] must be imposed on an interpretation in the neighborhood of each command.
</blockquote>

In 1969, [[Tony Hoare]] published a paper on [[Hoare logic]] seeded by Floyd's ideas, now sometimes collectively called ''[[axiomatic semantics]]''.<ref name="hoare">{{Cite journal
 |last=Hoare 
 |first=C. A. R. 
 |authorlink=Tony Hoare 
 |title=An axiomatic basis for computer programming 
 |doi=10.1145/363235.363259 
 |journal=[[Communications of the ACM]] 
 |volume=12 
 |issue=10 
 |pages=576–580 
 |date=October 1969 
 |s2cid=207726175 
 |doi-access=free 
 }}</ref>{{r|winskel}}

In the 1970s, the terms ''[[operational semantics]]'' and ''[[denotational semantics]]'' emerged.<ref name=winskel>{{cite book |last1=Winskel |first1=Glynn |title=The formal semantics of programming languages : an introduction |date=1993 |publisher=MIT Press |location=Cambridge, Mass. |isbn=978-0-262-23169-5 |page=[https://archive.org/details/formalsemanticso0000wins/page/n17 xv] |url=https://archive.org/details/formalsemanticso0000wins}}</ref>

==Overview==
The field of formal semantics encompasses all of the following:
*The definition of semantic models
*The relations between different semantic models
*The relations between different approaches to meaning
*The relation between computation and the underlying mathematical structures from fields such as [[mathematical logic|logic]], [[set theory]], [[model theory]], [[category theory]], etc.

It has close links with other areas of [[computer science]] such as [[programming language design]], [[type theory]], [[compiler]]s and [[interpreter (computing)|interpreters]], [[program verification]] and [[model checking]].

==Approaches==
There are many approaches to formal semantics; these belong to three major classes:

* '''[[Denotational semantics]]''',<ref name=Schmidt1986>{{cite book |author-first=David A.|author-last=Schmidt |title=Denotational Semantics: A Methodology for Language Development |publisher=William C. Brown Publishers |date=1986 |isbn=9780205104505}}</ref> whereby each phrase in the language is interpreted as a ''[[denotation (semiotics)|denotation]]'', i.e. a conceptual meaning that can be thought of abstractly.  Such denotations are often mathematical objects inhabiting a mathematical space, but it is not a requirement that they should be so.  As a practical necessity, denotations are described using some form of mathematical notation, which can in turn be formalized as a denotational metalanguage.  For example, denotational semantics of [[functional programming language|functional languages]] often translate the language into [[domain theory]]. Denotational semantic descriptions can also serve as compositional translations from a programming language into the denotational metalanguage and used as a basis for designing [[compiler]]s.
* '''[[Operational semantics]]''',<ref name=Plotkin1981>{{cite report |author-link=Gordon Plotkin|first=Gordon D.|last=Plotkin |title=A structural approach to operational semantics |series=Technical Report DAIMI FN-19 |publisher=Computer Science Department, [[Aarhus University]] |date=1981}}</ref> whereby the execution of the language is described directly (rather than by translation).  Operational semantics loosely corresponds to [[interpreter (computing)|interpretation]], although again the "implementation language" of the interpreter is generally a mathematical formalism.  Operational semantics may define an [[abstract machine]] (such as the [[SECD machine]]), and give meaning to phrases by describing the transitions they induce on states of the machine.  Alternatively, as with the pure [[lambda calculus]], operational semantics can be defined via syntactic transformations on phrases of the language itself;
* '''[[Axiomatic semantics]]''',<ref name=Goguen77>{{cite journal |author1-link=Joseph Goguen|author1-first=Joseph A.|author1-last=Goguen |author2-first=James W.|author2-last=Thatcher |author3-first=Eric G.|author3-last=Wagner |author4-first=Jesse B.|author4-last=Wright |title=Initial algebra semantics and continuous algebras |journal=[[Journal of the ACM]] |volume=24 |issue=1 |date=1977 |pages=68–95 |doi=10.1145/321992.321997|s2cid=11060837 |doi-access=free }}</ref> whereby one gives meaning to phrases by describing the ''[[axiom]]s'' that apply to them.  Axiomatic semantics makes no distinction between a phrase's meaning and the logical formulas that describe it; its meaning ''is'' exactly what can be proven about it in some logic.  The canonical example of axiomatic semantics is [[Hoare logic]].

Apart from the choice between denotational, operational, or axiomatic approaches, most variations in formal semantic systems arise from the choice of supporting mathematical formalism.{{cn|date=April 2024}}

==Variations==
Some variations of formal semantics include the following:

* '''[[Action semantics]]'''<ref name=Mosses1996>{{cite report |author-link=Peter Mosses|author-first=Peter D.|author-last=Mosses |date=1996 |title=Theory and practice of action semantics |publisher=[[Aarhus University]] |series=BRICS Report RS9653}}</ref> is an approach that tries to modularize denotational semantics, splitting the formalization process in two layers (macro and microsemantics) and predefining three semantic entities (actions, data and yielders) to simplify the specification;
* '''[[Algebraic semantics (computer science)|Algebraic semantics]]'''<ref name=Goguen77/> is a form of [[axiomatic semantics]] based on [[algebra]]ic laws for describing and reasoning about [[program semantics]] in a [[formal methods|formal]] manner. It also supports [[denotational semantics]] and [[operational semantics]];
* '''[[Attribute grammar]]s'''<ref>{{cite book |author1-first=Pierre|author1-last=Deransart |author2-first=Martin|author2-last=Jourdan |author3-first=Bernard|author3-last=Lorho |title="Attribute Grammars: Definitions, Systems and Bibliography |date=1988 |series=Lecture Notes in Computer Science 323 |publisher=[[Springer-Verlag]] |isbn=9780387500560}}</ref> define systems that systematically compute "[[metadata]]" (called ''attributes'') for the various cases of [[Syntax (programming languages)|the language's syntax]].  Attribute grammars can be understood as a denotational semantics where the target language is simply the original language enriched with attribute annotations.  Aside from formal semantics, attribute grammars have also been used for code generation in [[compiler]]s, and to augment [[Regular languages|regular]] or [[Context-free languages|context-free grammars]] with [[Context-sensitive languages|context-sensitive]] conditions;
* '''[[Categorical semantics|Categorical]] (or "functorial") semantics'''<ref name=Lawvere1963>{{cite journal |author-link=William Lawvere|author-first=F. William|author-last=Lawvere |title=Functorial semantics of algebraic theories |journal=[[Proceedings of the National Academy of Sciences of the United States of America]] |volume=50 |issue=5 |date=1963 |pages=869–872 |doi=10.1073/pnas.50.5.869|pmid=16591125 |pmc=221940 |bibcode=1963PNAS...50..869L |doi-access=free }}</ref> uses [[category theory]] as the core mathematical formalism. Categorical semantics is usually proven to correspond to some axiomatic semantics that gives a syntactic presentation of the categorical structures. Also, denotational semantics are often instances of a general categorical semantics;<ref>{{cite journal |author1=Andrzej Tarlecki |author2=[[Rod Burstall|Rod M. Burstall]] |author3=[[Joseph Goguen|Joseph A. Goguen]] |title=Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories |journal=[[Theoretical Computer Science]] |volume=91 |issue=2 |date=1991 |pages=239–264 |doi=10.1016/0304-3975(91)90085-G|doi-access=free }}</ref>
* '''[[Concurrency semantics]]'''<ref>{{cite conference |author1-first=Mark|author1-last=Batty |author2-first=Kayvan|author2-last=Memarian |author3-first=Kyndylan|author3-last=Nienhuis |author4-first=Jean|author4-last=Pichon-Pharabod |author5-first=Peter|author5-last=Sewell |title=The problem of programming language concurrency semantics |book-title=Proceedings of the European Symposium on Programming Languages and Systems |pages=283–307 |publisher=[[Springer Publishing|Springer]] |date=2015 |doi=10.1007/978-3-662-46669-8_12|doi-access=free |url=http://kar.kent.ac.uk/50271/1/c_concurrency_challenges.pdf }}</ref> is a catch-all term for any formal semantics that describes concurrent computations.  Historically important concurrent formalisms have included the [[actor model]] and [[process calculi]];
* '''[[Game semantics]]'''<ref name=Abramsky2009>{{cite book |author-link=Samson Abramsky|author-first=Samson|author-last=Abramsky |chapter=Semantics of interaction: An introduction to game semantics |title=Semantics and Logics of Computation |date=2009 |pages=1–32 |doi=10.1017/CBO9780511526619.002  |publisher=Cambridge University Press |isbn=9780521580571 |url=https://ora.ox.ac.uk/objects/uuid:ab3ece5b-cd8d-49e6-ba33-010ea4c1a1ac |editor1=Andrew M. Pitts |editor2=P. Dybjer}}</ref> uses a metaphor inspired by [[game theory]];
* '''[[Predicate transformer semantics]]''',<ref name=Dijkstra1975>{{cite journal |author-link=Edsger W. Dijkstra|author-first=Edsger W.|author-last=Dijkstra |date=1975 |title=Guarded commands, nondeterminacy and formal derivation of programs |journal=[[Communications of the ACM]] |volume=18 |issue=8 |pages=453–457 |doi=10.1145/360933.360975|s2cid=1679242 |doi-access=free }}</ref> developed by [[Edsger W. Dijkstra]], describes the meaning of a program fragment as the function transforming a [[postcondition]] to the [[precondition]] needed to establish it.

==Describing relationships==
For a variety of reasons, one might wish to describe the relationships between different formal semantics.  For example:
*To prove that a particular operational semantics for a language satisfies the logical formulas of an axiomatic semantics for that language.  Such a proof demonstrates that it is "sound" to reason about a particular (operational) ''interpretation strategy'' using a particular (axiomatic) ''proof system''.
*To prove that operational semantics over a high-level machine is related by a [[simulation]] with the semantics over a low-level machine, whereby the low-level abstract machine contains more primitive operations than the high-level abstract machine definition of a given language. Such a proof demonstrates that the low-level machine "faithfully implements" the high-level machine.

It is also possible to relate multiple semantics through [[abstraction (computer science)#Semantics|abstractions]] via the theory of [[abstract interpretation]].{{cn|date=April 2024}}

== See also ==
* [[Computational semantics]]
* [[Formal semantics (logic)]]
* [[Formal semantics (linguistics)]]
* [[Ontology]]
* [[Ontology (information science)]]
* [[Semantic equivalence]]
* [[Semantic technology]]

== References ==
{{reflist}}

== Further reading ==
; Textbooks
{{refbegin}}
*{{cite book |year=1967 |author-link=Robert W. Floyd |first=Robert W. |last=Floyd |chapter=Assigning Meanings to Programs |chapter-url=https://www.cs.tau.ac.il/~nachumd/term/FloydMeaning.pdf |editor-first=J.T. |editor-last=Schwartz |title=Mathematical Aspects of Computer Science |publisher=American Mathematical Society |isbn=0821867288 |pages=19–32 |url=https://books.google.com/books?id=ynigSICJflYC |series=Proceedings of Symposium on Applied Mathematics |volume=19 }}
*{{cite book |year=1990 |first=M. |last=Hennessy |authorlink = Matthew Hennessy|title=The semantics of programming languages: an elementary introduction using structural operational semantics |publisher=Wiley |isbn=978-0-471-92772-3}}
*{{cite book |year=1991 |author-link=Robert D. Tennent |first=Robert D. |last=Tennent |title=Semantics of Programming Languages |url=https://books.google.com/books?id=K7N7QgAACAAJ |publisher=Prentice Hall |isbn=978-0-13-805599-8}}
*{{cite book |year=1992 |author-link=Carl Gunter (computer scientist) |first=Carl |last=Gunter |title=Semantics of Programming Languages |publisher=MIT Press |isbn=0-262-07143-6 }}
*{{cite book |year=1992 |first1=H. R. |last1=Nielson |first2=Flemming |last2=Nielson |title=Semantics With Applications: A Formal Introduction |url=http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.pdf |publisher=Wiley |isbn=978-0-471-92980-2 |access-date=2011-05-27 |archive-date=2012-04-17 |archive-url=https://web.archive.org/web/20120417112149/http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.pdf |url-status=dead }}
*{{cite book |year=1993 |author-link=Glynn Winskel |first=Glynn |last=Winskel |title=The Formal Semantics of Programming Languages: An Introduction |publisher=MIT Press |isbn=0-262-73103-7 }}
*{{cite book |year=1995 |author-link=John C. Mitchell |last=Mitchell |first=John C. |url=http://www.lix.polytechnique.fr/~catuscia/teaching/cg520/papers_and_books/Mitchell_book.ps.gz |title=Foundations for Programming Languages |format=Postscript}}
*{{cite book |year=1995 |author-link=Kenneth Slonneger |first1=Kenneth |last1=Slonneger |author-link2=Barry L. Kurtz |first2=Barry L. |last2=Kurtz |title=Formal Syntax and Semantics of Programming Languages |publisher=Addison-Wesley |isbn=0-201-65697-3 |url=http://www.cs.uiowa.edu/~slonnegr/plf/Book/}}
*{{cite book |year=1998 |author-link=John C. Reynolds |first=John C. |last=Reynolds |title=Theories of Programming Languages |url=https://archive.org/details/theoriesofprogra0000reyn |url-access=registration |publisher=Cambridge University Press |isbn=0-521-59414-6 }}
*{{cite book |year=2006 |author-link=Robert Harper (computer scientist) |first=Robert |last=Harper |title=Practical Foundations for Programming Languages |url=https://www.cs.cmu.edu/~rwh/plbook/book.pdf |url-status=dead |archive-url=https://web.archive.org/web/20070627041059/https://www.cs.cmu.edu/~rwh/plbook/book.pdf |archive-date=2007-06-27 }} (Working draft)
*{{cite book  |first1=H. R. |last1=Nielson |first2=Flemming |last2=Nielson |title=Semantics with Applications: An Appetizer |url=https://books.google.com/books?id=oPi0yERDUeYC |date=2007 |publisher=Springer |isbn=978-1-84628-692-6}}
*{{cite book |year=2014 |author-link=Aaron Stump |first=Aaron |last=Stump |title=Programming Language Foundations |publisher=Wiley |isbn=978-1-118-00747-1 }}
*{{cite web  |author-link=Shriram Krishnamurthi |first=Shriram |last=Krishnamurthi |title=Programming Languages: Application and Interpretation |date=2012 |edition=2nd |url=https://cs.brown.edu/courses/cs173/2012/book/}}
; Lecture notes
*{{cite web |first=Glynn |last=Winskel |title=Denotational Semantics |publisher=University of Cambridge |url=http://www.cl.cam.ac.uk/~gw104/dens.pdf }}
{{refend}}

== External links ==
* {{cite book|last=Aaby|first=Anthony|title=Introduction to Programming Languages|year=2004|url=http://www.emu.edu.tr/aelci/Courses/D-318/D-318-Files/plbook/semantic.htm|url-status=dead|archive-url=https://web.archive.org/web/20150619164601/http://www.emu.edu.tr/aelci/Courses/D-318/D-318-Files/plbook/semantic.htm|archive-date=2015-06-19}} Semantics.

{{DEFAULTSORT:Semantics Of Programming Languages}}
[[Category:Formal methods]]
[[Category:Logic in computer science]]
[[Category:Formal specification languages| ]]
[[Category:Programming language semantics| ]]