Operational semantics: Difference between revisions

Revision as of 19:07, 4 March 2018

Latest revision as of 09:44, 29 July 2025

(42 intermediate revisions by 28 users not shown)

Line 1:

{{Short description|Category of formal programming language semantics}}

'''Operational semantics''' is a category of [[Semantics (computer science)|formal programming language semantics]] in which certain desired properties of a program, such as correctness, safety or security, are [[formal verification|verified]] by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms ([[denotational semantics]]). Operational semantics are classified in two categories: '''structural operational semantics''' (or '''small-step semantics''') formally describe how the ''individual steps'' of a [[computation]] take place in a computer-based system; by opposition '''natural semantics''' (or '''big-step semantics''') describe how the ''overall results'' of the executions are obtained. Other approaches to providing a [[formal semantics of programming languages]] include [[axiomatic semantics]] and [[denotational semantics]].

{{Semantics}}

'''Operational semantics''' is a category of [[SemanticsFormal (computer science)language|formal programming language]] [[Semantics (computer science)|semantics]] in which certain desired properties of a [[Computer program|program]], such as correctness, safety or security, are [[formal verification|verified]] by constructing proofs[[Mathematical proof|proof]]s from logical statements about its [[Execution (computing)|execution]] and procedures, rather than by attaching mathematical meanings to its terms ([[denotational semantics]]). Operational semantics are classified in two categories: '''structural operational semantics''' (or '''small-step semantics''') formally describe how the ''individual steps'' of a [[computation]] take place in a computer-based system; by opposition '''natural semantics''' (or '''big-step semantics''') describe how the ''overall results'' of the executions are obtained. Other approaches to providing a [[formal semantics of programming languages]] include [[axiomatic semantics]] and [[denotational semantics]].

The operational semantics for a programming language describes how a valid program is interpreted as sequences of computational steps.

These sequences then ''are'' the meaning of the program.

In the context of [[functional program]]s, the final step in a terminating

sequence returns the value of the program. (In general there can be many return values for a single program,

because the program could be [[Nondeterministic algorithm|nondeterministic]], and even for a deterministic program there can be many computation sequences since the semantics may not specify exactly what sequence of operations arrives at that value.)

The operational semantics for a [[programming language]] describes how a valid program is interpreted as sequences of computational steps. These sequences then ''are'' the meaning of the program. In the context of [[functional programming]], the final step in a terminating sequence returns the value of the program. (In general there can be many return values for a single program, because the program could be [[Nondeterministic algorithm|nondeterministic]], and even for a deterministic program there can be many computation sequences since the semantics may not specify exactly what sequence of operations arrives at that value.)

Perhaps the first formal incarnation of operational semantics was the use of the [[lambda calculus]] to define the semantics of [[LISP]].<ref>{{Cite web| title=Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I| author=[[John McCarthy (computer scientist)|John McCarthy]]| url=http://www-formal.stanford.edu/jmc/recursive.html| accessdate=2006-10-13| deadurl=yes| archiveurl=https://web.archive.org/web/20131004215327/http://www-formal.stanford.edu/jmc/recursive.html| archivedate=2013-10-04| df=}}</ref>

[[Abstract machine]]s in the tradition of the [[SECD machine]] are also closely related.

Perhaps the first formal incarnation of operational semantics was the use of the [[lambda calculus]] to define the semantics of [[LISPLisp (programming language)|Lisp]].<ref>{{Cite web| |title=Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I |last=McCarthy |first=John |author-link=[[John McCarthy (computer scientist)|John McCarthy]]| url=http://www-formal.stanford.edu/jmc/recursive.html| accessdate|access-date=2006-10-13| deadurl=yes|url-status=dead archiveurl|archive-url=https://web.archive.org/web/20131004215327/http://www-formal.stanford.edu/jmc/recursive.html| archivedate|archive-date=2013-10-04| df=}}</ref> [[Abstract machine]]s in the tradition of the [[SECD machine]] are also closely related.

== History ==

== 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 17 ⟶ 14:

<blockquote>

The meaning of a program in the strict language is explained in terms of a hypothetical computer

which performs the set of actions whichthat constitute the elaboration of that program. ([[#algol68|Algol68]], Section 2)

</blockquote>

Line 32 ⟶ 29:

== Approaches ==

[[Gordon Plotkin]] introduced the structural operational semantics, Robert Hieb and [[Matthias Felleisen]] and Robert Hieb the reduction contextssemantics,<ref name="felleisen-hieb-92">{{cite journal |title=The Revised Report on the Syntactic Theories of Sequential Control and State | journal=Theoretical Computer Science | last1=Felleisen | first1=M. | last2=Hieb | first2=R. |year=1992 doi|volume=103 |issue=2 |pages=235–271 |doi=10.1016/0304-3975(92)90014-7|doi-access= }}</ref> and [[Gilles Kahn]] the natural semantics.

=== 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]]) as a logical means to define operational semantics. The basic idea behind SOS is to define the behavior of a program in terms of the behavior of its parts, thus providing a structural, i.e., syntax-oriented and [[inductive definition|inductive]], view on operational semantics. An SOS specification defines the behavior of a program in terms of a (set of) [[State transition system|transition relation]](s). SOS specifications take the form of a set of [[inference rule]]s that define the valid transitions of a composite piece of syntax in terms of the transitions of its components.

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 63 ⟶ 59:

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 can run <math>C_1</math>, and then run <math>C_2</math>

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> with 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_1';C_2</math> in state <math>s'</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 89 ⟶ 85:

==== Reduction semantics ====

'''Reduction semantics''' is an alternative presentation of operational semantics. Its key ideas were first applied to purely functional [[call by name]] and [[call by value]] variants of the [[lambda calculus]] by [[Gordon Plotkin]] in 1975<ref>{{cite journal|last=Plotkin|first=Gordon|date=1975|title=Call-by-name, call-by-value and the λ-calculus|journal=Theoretical Computer Science|volume=1|issue=2|pages=125–159|doi=10.1016/0304-3975(75)90017-1|url=https://www.sciencedirect.com/science/article/pii/0304397575900171/pdf?md5=db2e67c1ada7163a28f124934b483f3a&pid=1-s2.0-0304397575900171-main.pdf|access-date=July 22, 2021|doi-access=free}}</ref> and generalized to higher-order functional languages with imperative features by [[Matthias Felleisen]] in his 1987 dissertation.<ref>{{cite thesis|type=PhD|last=Felleisen|first=Matthias|date=1987|title=The calculi of Lambda-v-CS conversion: a syntactic theory of control and state in imperative higher-order programming languages|publisher=Indiana University|url=https://www2.ccs.neu.edu/racket/pubs/dissertation-felleisen.pdf|access-date=July 22, 2021}}</ref> The method was further elaborated by Matthias Felleisen and Robert Hieb in 1992 into a fully [[equational theory]] for [[control flow|control]] and [[program state|state]].<ref name="felleisen-hieb-92" /> The phrase “reduction semantics” itself was first coined by Felleisen and [[Daniel P. Friedman]] in a PARLE 1987 paper.<ref>{{cite conference|last1=Felleisen|first1=Matthias|last2=Friedman|first2=Daniel P.|date=1987|title=A Reduction Semantics for Imperative Higher-Order Languages|book-title=Proceedings of the Parallel Architectures and Languages Europe|volume=1|pages=206–223|conference=International Conference on Parallel Architectures and Languages Europe|publisher=Springer-Verlag|doi=10.1007/3-540-17945-3_12}}</ref>

'''Reduction semantics''' are an alternative presentation of operational semantics using so-called reduction contexts. The method was introduced by Robert Hieb and [[Matthias Felleisen]] in 1992 as a technique for formalizing an [[equational theory]] for [[control flow|control]] and [[program state|state]]. For example, the grammar of a simple [[call-by-value]] [[lambda calculus]] and its contexts can be given as:

Reduction semantics are given as a set of ''reduction rules'' that each specify a single potential reduction step. For example, the following reduction rule states that an assignment statement can be reduced if it sits immediately beside its variable declaration:

<math>

e = v \;|\; (e\; e) \;|\; x \quad\quad v = \lambda x.e \quad\quad C = \left[\,\right] \;|\; (C\; e) \;|\; (v\; C)

<math>\mathbf{let\ rec}\ x = v_1\ \mathbf{in}\ x \leftarrow v_2;\ e\ \ \longrightarrow\ \ \mathbf{let\ rec}\ x = v_2\ \mathbf{in}\ e</math>

</math>

To get an assignment statement into such a position it is “bubbled up” through function applications and the right-hand side of assignment statements until it reaches the proper point. Since intervening <math>\mathbf{let}</math> expressions may declare distinct variables, the calculus also demands an extrusion rule for <math>\mathbf{let}</math> expressions. Most published uses of reduction semantics define such “bubble rules” with the convenience of evaluation contexts. For example, the grammar of evaluation contexts in a simple [[call by value]] language can be given as

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>

E ::= [\,]\ \big|\ v\ E\ \big|\ E\ e\ \big|\ x \leftarrow E

(\lambda x.e)\; v \longrightarrow e\,\left[x / v\right] \quad (\mathrm{\beta})

\ \big|\ \mathbf{let\ rec}\ x = v\ \mathbf{in}\ E\ \big|\ E;\ e

</math>

where <math>e</math> denotes arbitrary expressions and <math>v</math> denotes fully-reduced values. Each evaluation context includes exactly one hole <math>[\,]</math> into which a term is plugged in a capturing fashion. The shape of the context indicates with this hole where reduction may occur. To describe “bubbling” with the aid of evaluation contexts, a single axiom suffices:

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.

<math>E[\,x \leftarrow v;\ e\,]\ \ \longrightarrow\ \ x \leftarrow v;\ E[\,e\,] \qquad \text{(lift assignments)}</math>

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.}}</ref> [[design by contract|contract systems]], and other language features.

This single reduction rule is the lift rule from Felleisen and Hieb's lambda calculus for assignment statements. The evaluation contexts restrict this rule to certain terms, but it is freely applicable in any term, including under lambdas.

=== Big-step semantics ===

Following Plotkin, showing the usefulness of a calculus derived from a set of reduction rules demands (1) a Church-Rosser lemma for the single-step relation, which induces an evaluation function, and (2) a Curry-Feys standardization lemma for the transitive-reflexive closure of the single-step relation, which replaces the non-deterministic search in the evaluation function with a deterministic left-most/outermost search. Felleisen showed that imperative extensions of this calculus satisfy these theorems. Consequences of these theorems are that the equational theory—the symmetric-transitive-reflexive closure—is a sound reasoning principle for these languages. However, in practice, most applications of reduction semantics dispense with the calculus and use the standard reduction only (and the evaluator that can be derived from it).

==== Natural semantics ====

Reduction semantics are particularly useful given the ease by which evaluation contexts can model state or unusual control constructs (e.g., [[first-class continuations]]). In addition, reduction semantics have been used to model [[Object-oriented programming|object-oriented]] languages,<ref>{{cite book|title=A Theory of Objects|last1=Abadi|first1=M.|last2=Cardelli|first2=L.|date=8 September 2012|publisher=Springer |isbn=9781441985989|url=https://books.google.com/books?id=AgzSBwAAQBAJ&q=%22operational+semantics%22}}</ref> [[design by contract|contract systems]], exceptions, futures, call-by-need, and many other language features. A thorough, modern treatment of reduction semantics that discusses several such applications at length is given by Matthias Felleisen, Robert Bruce Findler and Matthew Flatt in ''Semantics Engineering with PLT Redex''.<ref>{{cite book|last1=Felleisen|first1=Matthias|last2=Findler|first2=Robert Bruce|last3=Flatt|first3=Matthew|title=Semantics Engineering with PLT Redex|year=2009|publisher=The MIT Press|isbn=978-0-262-06275-6|url=https://mitpress.mit.edu/9780262062756/semantics-engineering-with-plt-redex/}}</ref>

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]</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]].

=== Big-step semantics ===

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.

==== Natural semantics ====

Big-step structural operational semantics is also known under the names '''natural semantics''', '''relational semantics''' and '''evaluation semantics'''.<ref>[httphttps://web.archive.org/web/20131019133339/https://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 (programming language)|ML]].

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.<ref>{{cite book|last1=Nipkow|first1=Tobias|last2=Klein|first2=Gerwin|date=2014|title=Concrete Semantics|pages=101–102|doi=10.1007/978-3-319-10542-0|url=http://concrete-semantics.org/concrete-semantics.pdf|access-date=Mar 13, 2024|doi-access=free|isbn=978-3-319-10541-3 }}</ref>

A big-step semantics describes in a divide-and-conquer manner how final evaluation results of language constructs can be obtained by combining the evaluation results of their syntactic counterparts (subexpressions, substatements, etc.).

Line 129 ⟶ 123:

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 ofover the details and order of evaluation. In the case of instrumented operational semantics, this allows the operational semantics to track and the semanticist to state and prove more accurate theorems about the run-time behaviour of the language. These properties make small-step semantics more convenient when proving [[type soundness]] of a type system against an operational semantics.<ref name="leroy-coinductivebigstep" />

== See also ==

* [[Algebraic semantics (computer science)|Algebraic semantics]]

* [[Axiomatic semantics]]

Line 139 ⟶ 132:

== References ==

{{reflistReflist}}

* [[Gilles Kahn]]. "Natural Semantics". ''Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science''. Springer-Verlag. London. 1987.

== Further reading ==

* <cite id=plotkin81> [[Gordon Plotkin|Gordon D. Plotkin.]] [http://citeseer.ist.psu.edu/673965.html A Structural Approach to Operational Semantics]. (1981) Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark. (Reprinted with corrections in J. Log. Algebr. Program. 60-61: 17-139 (2004), [http://homepages.inf.ed.ac.uk/gdp/publications/sos_jlap.pdf preprint]). </cite>

* [[Gilles Kahn]]. "Natural Semantics". ''Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science''. Springer-Verlag. London. 1987.

* <cite id=plotkin04> [[Gordon Plotkin|Gordon D. Plotkin.]] The Origins of Structural Operational Semantics. J. Log. Algebr. Program. 60-61:3-15, 2004. ([http://homepages.inf.ed.ac.uk/gdp/publications/Origins_SOS.pdf preprint]). </cite>

* <cite id=plotkin81> [[Gordon Plotkin|Gordon D. Plotkin.]] [http://citeseer.ist.psu.edu/673965.html A Structural Approach to Operational Semantics]. (1981) Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark. (Reprinted with corrections in J. Log. Algebr. Program. 60-61: 17-139 (2004), ([http://homepages.inf.ed.ac.uk/gdp/publications/sos_jlap.pdf preprint]). </cite>

* <cite id=scott70> [[Dana Scott|Dana S. Scott.]] Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2, Oxford University, 1970.</cite>

* <cite id=plotkin04> [[Gordon Plotkin|Gordon D. Plotkin.]] The Origins of Structural Operational Semantics. J. Log. Algebr. Program. 60-61:3-15, 2004. ([http://homepages.inf.ed.ac.uk/gdp/publications/Origins_SOS.pdf preprint]). </cite>

* <cite id=algol68> [[Adriaan van Wijngaarden]] et al. [[ALGOL 68|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=scott70> [[Dana Scott|Dana S. Scott.]] Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2, Oxford University, 1970.</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>

* <cite id=algol68> [[Adriaan van Wijngaarden]] et al. [[ALGOL 68|Revised Report on the Algorithmic Language [[ALGOL 68]]. IFIP. 1968.]] ([httphttps://vesteinjemarch.arbnet/algol68-phys.unirevised-dortmund.de/~wb/RR/rrreport.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>

==External links==

*{{Commons category-inline}}

{{Authority control}}

[[Category:Operational semantics| ]]

[[Category:Formal specification languages]]

[[Category:Logic in computer science]]

[[Category:Programming language semantics]]

[[Category:Operational semantics| ]]