View source for Semantics (computer science)

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

In [[Programming language theory|programming language theory]], '''semantics''' is the rigorous mathematical study of the meaning of [[Programming language|programming language]]s.<ref>{{cite book |first=Joseph A.|last=Goguen |chapter=Semantics of computation |title=Category Theory Applied to Computation and Control |series=Lecture Notes in Computer Science |publisher=[[Company: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|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 platform; hence creating a [[Model of computation|model of computation]].

==History==

In 1967, [[Biography:Robert W. Floyd|Robert W. Floyd]] publishes the paper ''Assigning meanings to programs''; his chief aim is "a rigorous standard for proofs about computer programs, including [[Formal verification|proofs of correctness]], equivalence, and termination".<ref name=floyd>{{cite book |year=1967 |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 writes:{{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, [[Biography:Tony Hoare|Tony Hoare]] publishes a paper on [[Hoare logic]] seeded by Floyd's ideas, now sometimes collectively called ''[[Axiomatic semantics|axiomatic semantics]]''.<ref name="hoare">{{Cite journal
 |last=Hoare 
 |first=C. A. R. 
 |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 
 |url=https://dl.acm.org/doi/pdf/10.1145/363235.363259
|doi-access=free 
 }}</ref>{{r|winskel}}

In the 1970s, the terms ''[[Operational semantics|operational semantics]]'' and ''[[Denotational semantics|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|set theory]], [[Model theory|model theory]], [[Category theory|category theory]], etc.

It has close links with other areas of [[Computer science|computer science]] such as programming language design, [[Type theory|type theory]], [[Compiler|compiler]]s and [[Interpreter (computing)|interpreters]], program verification and [[Model checking|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'', 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 languages often translate the language into [[Domain theory|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|compiler]]s.
* '''[[Operational semantics]]''',<ref name=Plotkin1981>{{cite report |first=Gordon D.|last=Plotkin |title=A structural approach to operational semantics |series=Technical Report DAIMI FN-19 |publisher=Computer Science Department, [[Organization:Aarhus University|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|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|lambda calculus]], operational semantics can be defined via syntactic transformations on phrases of the language itself;
* '''[[Axiomatic semantics]]''',<ref name=Goguen77>{{cite journal |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|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.

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

* '''[[Action semantics]]'''<ref name=Mosses1996>{{cite report |author-first=Peter D.|author-last=Mosses |date=1996 |title=Theory and practice of action semantics |publisher=[[Organization:Aarhus University|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|axiomatic semantics]] based on [[Algebra|algebra]]ic laws for describing and reasoning about program semantics in a [[Formal methods|formal]] manner. It also supports [[Denotational semantics|denotational semantics]] and [[Operational semantics|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=[[Physics:Springer-Verlag|Springer-Verlag]] |isbn=9780387500560}}</ref> define systems that systematically compute "[[Metadata|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|compiler]]s, and to augment regular or context-free grammars with context-sensitive conditions;
* '''Categorical (or "functorial") semantics'''<ref name=Lawvere1963>{{cite journal |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|category theory]] as the core mathematical formalism. A 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=[[Biography:Rod Burstall|Rod M. Burstall]] |author3=[[Biography: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=[[Company:Springer Publishing|Springer]] |date=2015 |doi=10.1007/978-3-662-46669-8_12|doi-access=free }}</ref> is a catch-all term for any formal semantics that describes concurrent computations.  Historically important concurrent formalisms have included the [[Actor model|actor model]] and process calculi;
* '''[[Game semantics]]'''<ref name=Abramsky2009>{{cite book |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|game theory]];
* '''[[Predicate transformer semantics]]''',<ref name=Dijkstra1975>{{cite journal |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 [[Biography:Edsger W. Dijkstra|Edsger W. Dijkstra]], describes the meaning of a program fragment as the function transforming a [[Postcondition|postcondition]] to the [[Precondition|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|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|abstract interpretation]].

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

== References ==
{{reflist}}

== Further reading ==
; Textbooks
{{refbegin}}
*{{cite book |year=1967 |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 |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 |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 |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 |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 |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 |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 |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 |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 |first=Aaron |last=Stump |title=Programming Language Foundations |publisher=Wiley |isbn=978-1-118-00747-1 }}
*{{cite web  |first=Shriram |last=Krishnamurthi |title=Programming Languages: Application and Interpretation |date=2012 |edition=2nd |url=http://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| ]]

{{Sourceattribution|Semantics (computer science)}}