This single reduction rule is the lift rule from Felleisen and Hieb's lambda calculus for assignment statements. The evaluation contexts restrict this rule to certain terms, but it is freely applicable in any term, including under lambdas.
Following Plotkin, showing the usefulness of such 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. MostHowever, 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).
TheReduction techniquesemantics isare particularly useful forgiven the ease inby which reductionevaluation contexts can model state or unusual control constructs (e.g., [[first-class 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. 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/books/semantics-engineering-plt-redex}}</ref>
