Content deleted Content added
Jerryobject (talk | contribs) WP:LINKs: add, updates, fix-cut needless WP:PIPE (WP:NOPIPE). Cut needless carriage returns in: sentences, paragraphs. WP:REFerence WP:CITation parameters respace from source template. MOS:FIRSTABBReviations define before WP:ABBRs in parentheses. |
direct link & spaces |
||
Line 6:
== History ==
The concept of operational semantics was used for the first time in defining the semantics of [[Algol 68]].
The following statement is a quote from the revised ALGOL 68 report:
Line 30 ⟶ 29:
=== Small-step semantics ===
==== Structural operational semantics ====
'''Structural operational semantics''' (SOS, also called '''structured operational semantics''' or '''small-step semantics''') was introduced by [[Gordon Plotkin]] in ([[#plotkin81|Plotkin81]])
For a simple example, we consider part of the semantics of a simple programming language; proper illustrations are given in [[#plotkin81|Plotkin81]] and [[#hennessybook|Hennessy90]], and other textbooks. Let <math>C_1, C_2</math> range over programs of the language, and let <math>s</math> range over states (e.g. functions from memory locations to values). If we have expressions (ranged over by <math>E</math>), values {{nobreak|(<math>V</math>)}} and locations (<math>L</math>), then a memory update command would have semantics:
Line 58 ⟶ 56:
Informally, the first rule says that,
if program <math>C_1</math> in state <math>s</math> finishes in state <math>s'</math>, then the program <math>C_1;C_2</math> in state <math>s</math> will reduce to the program <math>C_2</math> in state <math>s'</math>.
(You can think of this as formalizing "You
using the resulting memory store.)
The second rule says that
if the program <math>C_1</math> in state <math>s</math> can reduce to the program <math>C_1'</math>
(You can think of this as formalizing the principle for an optimizing compiler:
"You are allowed to transform <math>C_1</math> as if it were stand-alone, even if it is just the
Line 90 ⟶ 88:
</math>
The contexts <math>C</math> include a hole <math>\left[\,\right]</math> where a term can be plugged in. The shape of the contexts indicate where reduction can occur (i.e., a term can be plugged into a term). To describe a semantics for this language, axioms or reduction rules are provided:
<math>
Line 98 ⟶ 94:
</math>
This single axiom is the beta rule from the lambda calculus. The reduction contexts show how this rule composes with more complicated terms. In particular, this rule can trigger for the argument position of an application like <math>((\lambda x.x \; \lambda x.x) \lambda x.(x\;x))</math> because there is a context <math>([\,]\; \lambda x.(x\;x))</math> that matches the term. In this case, the contexts uniquely decompose terms so that only one reduction is possible at any given step. Extending the axiom to match the reduction contexts gives the ''compatible closure''. Taking the reflexive, transitive closure of this relation gives the ''reduction relation'' for this language.
The technique is useful for the ease in which reduction contexts can model state or control constructs (e.g., [[continuations]]). In addition, reduction semantics have been used to model [[object-oriented]] languages,<ref>{{cite book|title=A Theory of Objects|last1=Abadi|first1=M.|last2=Cardelli|first2=L.|date=8 September 2012|isbn=9781441985989|url=https://books.google.com/books?id=AgzSBwAAQBAJ&q=%22operational+semantics%22}}</ref> [[design by contract|contract systems]], and other language features.
===
Big-step structural operational semantics is also known under the names '''natural semantics''', '''relational semantics''' and '''evaluation semantics'''.<ref>[http://fsl.cs.illinois.edu/images/6/63/CS422-Spring-2010-BigStep.pdf University of Illinois CS422]</ref> Big-step operational semantics was introduced under the name ''natural semantics'' by [[Gilles Kahn]] when presenting Mini-ML, a pure dialect of
▲==== Natural semantics ====
▲Big-step structural operational semantics is also known under the names '''natural semantics''', '''relational semantics''' and '''evaluation semantics'''.<ref>[http://fsl.cs.illinois.edu/images/6/63/CS422-Spring-2010-BigStep.pdf University of Illinois CS422]</ref> Big-step operational semantics was introduced under the name ''natural semantics'' by [[Gilles Kahn]] when presenting Mini-ML, a pure dialect of the [[ML language]].
One can view big-step definitions as definitions of functions, or more generally of relations, interpreting each language construct in an appropriate ___domain. Its intuitiveness makes it a popular choice for semantics specification in programming languages, but it has some drawbacks that make it inconvenient or impossible to use in many situations, such as languages with control-intensive features or concurrency.
Line 124 ⟶ 113:
The main disadvantage of big-step semantics is that non-terminating ([[divergence (computer science)|diverging]]) computations do not have an inference tree, making it impossible to state and prove properties about such computations.<ref name="leroy-coinductivebigstep" />
Small-step semantics give more control
== See also ==
* [[Algebraic semantics (computer science)|Algebraic semantics]]
* [[Axiomatic semantics]]
Line 136 ⟶ 124:
{{Reflist}}
*[[Gilles Kahn]]. "Natural Semantics". ''Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science''. Springer-Verlag. London. 1987.
*<cite id=plotkin81>
*<cite id=plotkin04>
*<cite id=scott70>
*<cite id=algol68> [[Adriaan van Wijngaarden]] et al. Revised Report on the Algorithmic Language [[ALGOL 68]]. IFIP. 1968. ([http://vestein.arb-phys.uni-dortmund.de/~wb/RR/rr.pdf]{{dead link|date=March 2018 |bot=InternetArchiveBot |fix-attempted=yes}})</cite>
*<cite id=hennessybook>[[Matthew Hennessy]]. Semantics of Programming Languages. Wiley, 1990. [https://www.cs.tcd.ie/matthew.hennessy/splexternal2015/resources/sembookWiley.pdf available online].</cite>
| |||