Operational semantics: Difference between revisions

Content deleted Content added
Reduction semantics: Matthias Felleisen here. The existing description was fundamentally wrong. An upset reader shared this link with me so I decided to put in 10 minutes to eliminate the worst conceptual mistakes.
Reduction semantics: Convert in-text references to papers into references
Line 29:
 
== Approaches ==
[[Gordon Plotkin]] introduced the structural operational semantics, Robert Hieb and [[Matthias Felleisen]] the reduction contexts,<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 |volume=103 |issue=2 |pages=235–271 |doi=10.1016/0304-3975(92)90014-7|doi-access=free }}</ref> and [[Gilles Kahn]] the natural semantics.
 
=== Small-step semantics ===
Line 85:
 
==== Reduction semantics ====
'''Reduction semantics''' is an alternative presentation of operational semantics. ItIts iskey dueideas were first applied to purely functional [[Gordoncall Plotkinby name]]'s 1975and paper[[call onby reasoningvalue]] aboutvariants functionalof languagesthe using[[lambda callcalculus]] by [[Gordon Plotkin]] in 1975<ref>{{cite journal|last=Plotkin|first=Gordon|date=1975|title=Call-by-name or, call-by-value with variants ofand the lambda λ-calculus|journal=Theoretical thatComputer areScience|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 sound22, for2021}}</ref> theseand parametergeneralized to higher-passingorder implementationsfunctional andlanguages with imperative features by [[Matthias Felleisen]]'s in his 1987 dissertation.<ref>{{cite research,thesis|type=PhD|last=Felleisen|first=Matthias|date=1987|title=The withcalculi whichof helambda-nu-cs constructedconversion: matchinga variantssyntactic theory of thecontrol lambdaand calculusstate forin extensions ofimperative higher-order functionalprogramming languages|publisher=Indiana withUniversity|url=https://www2.ccs.neu.edu/racket/pubs/dissertation-felleisen.pdf|access-date=July imperative features (assignment statements22, control operators, delimited control, and so on).2021}}</ref> The method was cleanedfurther upelaborated by Robert Hieb and [[Matthias Felleisen]] in 1992 into a completelyfully [[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 19861987 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>
 
For example, an assignment statement can be reduced if it sits next to its variable declaration: