In the last lecture we defined a semantics for our language of arithmetic expressions using a small-step evaluation relation (and its reflexive and transitive closure ). In this note we will explore an alternative approach--large-step operational semantics--which yields the final result of evaluating an expression directly.
Defining a large-step semantics boils down to specifying a relation that captures the evaluation of an expression. The relation has the following type: We write to indicate that In other words, the expression with store evaluates in one big step to the final store and integer .
We define the relation inductively, using inference rules: To illustrate the use of these rules, consider the following proof tree, which shows that evaluating using a store such that yields and as a result: A closer look to this structure reveals the relation between small step and large-step evaluation: a depth-first traversal of the large-step proof tree yields the sequence of one-step transitions in small-step evaluation.
Equivalence of Semantics
A natural question to ask is whether the small-step and large-step semantics are equivalent. The next theorem answers this question affirmatively.
Theorem (Equivalence of semantics). For all expressions , stores and , and integers we have: To streamline the proof, we will work with the following definition of the multi-step relation: Proof sketch. We show each direction separately.
: We want to prove that the following property holds for all expressions : We proceed by structural induction on . We have to consider each of the possible axioms and inference rules for constructing an expression.
CASE Assume that That is, there is some derivation in the large-step operational semantics whose conclusion is There is only one rule whose conclusion matches the configuration the large-step rule . Thus, we have and By the small-step rule , we also have By the and rules, we conclude that , which finishes the case.
CASE: Assume that There is only one rule whose conclusion matches the large-step rule . Thus, we have and and so by the rule.
CASE: This is an inductive case. We want to prove that if and hold, then
also holds. Let’s write out , , and explicitly. Assume that and hold. Also assume that there exist and such that We need to show that We assumed that This means that there is some derivation whose conclusion is By inspection, we see that only one rule has a conclusion of this form: the rule. Thus, the last rule used in the derivation was and it must be the case that and hold for some and with .
By the induction hypothesis , as , we must have . Likewise, by induction hypothesis , we have By Lemma 1 below, we have and by another application of Lemma 1 we have: Then, using the small-step rule and the multi-step rule, we have: Finally, by two applications of Lemma 2, we obtain , which finishes the case.
: We proceed by induction on the derivation of with a case analysis on the last rule used.
CASE: Then and . We immediately have by the large-step rule .
CASE: Then and . In this case, the induction hypothesis gives . The result follows from Lemma 3 below.
Lemma 1. If , then the following hold:
Proof. Omitted; try it as an exercise.
Lemma2. If and , then . Proof. Omitted; try it as an exercise
Lemma 3. If and , then . Proof. Omitted; try it as an exercise.
