Operational semantics: Difference between revisions

Revision as of 22:27, 14 July 2021

Revision as of 14:17, 22 July 2021

Line 85:

==== Reduction semantics ====

'''Reduction semantics''' areis an alternative presentation of operational semantics. It is due to [[Gordon Plotkin]]'s 1975 paper on reasoning about functional languages using socall-calledby-name reductionor contextscall-by-value with variants of the lambda calculus that are sound for these parameter-passing implementations and [[Matthias Felleisen]]'s 1987 dissertation research, with which he constructed matching variants of the lambda calculus for extensions of higher-order functional languages with imperative features (assignment statements, control operators, delimited control, and so on). The method was introducedcleaned up by Robert Hieb and [[Matthias Felleisen]] in 1992 asinto a technique for formalizing ancompletely [[equational theory]] for [[control flow|control]] and [[program state|state]]. ForThe example,phrase thewas grammarcoined ofby aFelleisen simpleand [[call-by-value]]Friedman [[lambda| calculusDaniel Friedman]] andin itsa contextsPARLE can1986 be givenpaper. as:

For example, an assignment statement can be reduced if it sits next to 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>

let rec x = v_1 in x <- v_2; e ---> let rec x = v_2 in e

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:

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 let expressions may declare distinct variables, the calculus also demands an extrusion rule for let expressions.

<math>

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

</math>

Most published formulations of the calculus show "bubble rules" with the convenience of evaluation contexts. For example, the grammar of the contexts in a simple [[call-by-value]] language (based on lambda syntax) and its evaluation contexts can be given as:

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.

E = [] | v E | E e | x <- E | let rec x = v in E | E; e

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.

The evaluation contexts <math>C</math> include a hole <math>\left[\,\right]</math> whereinto which a term can beis plugged in a capturing fashion. The shape of the contexts indicate with this hole where reduction canmay occur (i.e., a term can be plugged into a term). To describe a semantics for this language"bubbling", axioms or reductiona rulessingle areaxiom providedsuffices:

E[ x <- v; e ] ---> x <- v; E[e] (lift assignments)

This single axiom is the lift axion from Felleisen and Hieb's lambda calculus for assignment statements. The evaluation contexts restricts this redex to certain terms but it is freely applicable in any term, including below lambdas.

Following Plotkin, showing the usefulness of such a calculus demands: (1) a Church-Rosser lemma for the single-step relation, which induces an evaluation function; (2) a Curry-Feys standardization lemma for the transitive-reflexive closure of the singe-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. Most application of reduction semantics dispense with the calculus and use the standard reduction only.

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]], exceptions, futures, call-by-need, and many other language features.

===Big-step semantics===