Operational semantics: Difference between revisions

Revision as of 19:02, 25 July 2021

Revision as of 13:30, 13 August 2021

Line 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 lambdaLambda-nuv-csCS 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 [[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 immediately beside its variable declaration: