Operational semantics: Difference between revisions

Revision as of 23:04, 22 July 2021

Revision as of 23:46, 22 July 2021

Line 87:

'''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}}</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-nu-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 Robert Hieb and Matthias Felleisen 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 [[Friedman | Daniel 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 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 nextimmediately tobeside its variable declaration:

<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>

To get an assignment statement into such a position it is "bubbled“bubbled up"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

<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:

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

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

</math>

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

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

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

The evaluation contexts include a hole <math>\left[\,\right]</math> into which a term is plugged in a capturing fashion. The shape of the contexts indicate with this hole where reduction may occur. To describe "bubbling", a single axiom suffices:

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

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

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 singesingle-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---thetheory—the symmetric-transitive-reflexive closure---isclosure—is a sound reasoning principle for these languages. Most applicationapplications of reduction semantics dispense with the calculus and use the standard reduction only.

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.