Revision as of 20:56, 5 January 2025 edit The Hurdy Gurdy Man (talk \| contribs) 287 edits m →Further reading: Fixed dead link. ← Previous edit		Latest revision as of 09:44, 29 July 2025 edit undo Onel5969 (talk \| contribs) Autopatrolled, Extended confirmed users, Page movers, New page reviewers, Pending changes reviewers, Rollbackers 993,160 edits m Disambiguating links to Object-orientation (link changed to Object-oriented programming) using DisamAssist.
Line 106: 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). 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 semantics===

Operational semantics: Difference between revisions