Acknowledgements
This material is taken verbatim from Software Foundations V4.0
Copyright (c) 2016
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
Assumed Knowledge:
* TODO
Learning Outcomes:
* TODO
The evaluators we have seen so far (for
aexps,
bexps,
commands, ...) have been formulated in a "bigstep" style: they
specify how a given expression can be evaluated to its final
value (or a command plus a store to a final store) "all in one big
step."
This style is simple and natural for many purposes — indeed,
Gilles Kahn, who popularized it, called it
natural semantics.
But there are some things it does not do well. In particular, it
does not give us a natural way of talking about
concurrent
programming languages, where the semantics of a program — i.e.,
the essence of how it behaves — is not just which input states
get mapped to which output states, but also includes the
intermediate states that it passes through along the way, since
these states can also be observed by concurrently executing code.
Another shortcoming of the bigstep style is more technical, but
critical in many situations. Suppose we want to define a variant
of Imp where variables could hold
either numbers
or lists of
numbers. In the syntax of this extended language, it will be
possible to write strange expressions like
2 + nil, and our
semantics for arithmetic expressions will then need to say
something about how such expressions behave. One possibility is
to maintain the convention that every arithmetic expressions
evaluates to some number by choosing some way of viewing a list as
a number — e.g., by specifying that a list should be interpreted
as
0 when it occurs in a context expecting a number. But this
is really a bit of a hack.
A much more natural approach is simply to say that the behavior of
an expression like
2+nil is
undefined — i.e., it doesn't
evaluate to any result at all. And we can easily do this: we just
have to formulate
aeval and
beval as
Inductive propositions
rather than Fixpoints, so that we can make them partial functions
instead of total ones.
Now, however, we encounter a serious deficiency. In this
language, a command might fail to map a given starting state to
any ending state for
two quite different reasons: either because
the execution gets into an infinite loop or because, at some
point, the program tries to do an operation that makes no sense,
such as adding a number to a list, so that none of the evaluation
rules can be applied.
These two outcomes — nontermination vs. getting stuck in an
erroneous configuration — are quite different. In particular, we
want to allow the first (permitting the possibility of infinite
loops is the price we pay for the convenience of programming with
general looping constructs like
while) but prevent the
second (which is just wrong), for example by adding some form of
typechecking to the language. Indeed, this will be a major
topic for the rest of the course. As a first step, we need a way
of presenting the semantics that allows us to distinguish
nontermination from erroneous "stuck states."
So, for lots of reasons, we'd like to have a finergrained way of
defining and reasoning about program behaviors. This is the topic
of the present chapter. We replace the "bigstep"
eval relation
with a "smallstep" relation that specifies, for a given program,
how the "atomic steps" of computation are performed.
A Toy Language
To save space in the discussion, let's go back to an
incredibly simple language containing just constants and
addition. (We use single letters —
C and
P (for Command and
Plus) — as constructor names, for brevity.) At the end of the
chapter, we'll see how to apply the same techniques to the full
Imp language.
Here is a standard evaluator for this language, written in
the bigstep style that we've been using up to this point.
Here is the same evaluator, written in exactly the same
style, but formulated as an inductively defined relation. Again,
we use the notation
t ⇓ n for "
t evaluates to
n."
t_{1} ⇓ n_{1} 

t_{2} ⇓ n_{2} 
(E_Plus)


P t_{1} t_{2} ⇓ n_{1} + n_{2} 

Reserved Notation " t '
⇓' n " (
at level 50,
left associativity).
Inductive eval :
tm → nat → Prop :=
Module SimpleArith1.
Now, here is the corresponding
smallstep evaluation relation.

(ST_PlusConstConst)


P (C n_{1}) (C n_{2}) ⇒ C (n_{1} + n_{2}) 

t_{1} ⇒ t_{1}' 
(ST_Plus1)


P t_{1} t_{2} ⇒ P t_{1}' t_{2} 

t_{2} ⇒ t_{2}' 
(ST_Plus2)


P (C n_{1}) t_{2} ⇒ P (C n_{1}) t_{2}' 

Things to notice:
 We are defining just a single reduction step, in which
one P node is replaced by its value.
 Each step finds the leftmost P node that is ready to
go (both of its operands are constants) and rewrites it in
place. The first rule tells how to rewrite this P node
itself; the other two rules tell how to find it.
 A term that is just a constant cannot take a step.
Let's pause and check a couple of examples of reasoning with
the
step relation...
If
t_{1} can take a step to
t_{1}', then
P t_{1} t_{2} steps
to
P t_{1}' t_{2}:
Exercise: 1 star (test_step_2)
Righthand sides of sums can take a step only when the
lefthand side is finished: if
t_{2} can take a step to
t_{2}',
then
P (C n) t_{2} steps to
P (C n)
t_{2}':
☐
Relations
We will be working with several different singlestep relations,
so it is helpful to generalize a bit and state a few definitions
and theorems about relations in general. (The optional chapter
Rel.v develops some of these ideas in a bit more detail; it may
be useful if the treatment here is too dense.)
A
binary relation on a set
X is a family of propositions
parameterized by two elements of
X — i.e., a proposition about
pairs of elements of
X.
Our main examples of such relations in this chapter will be
the singlestep reduction relation,
⇒, and its multistep
variant,
⇒* (defined below), but there are many other
examples — e.g., the "equals," "less than," "less than or equal
to," and "is the square of" relations on numbers, and the "prefix
of" relation on lists and strings.
One simple property of the
⇒ relation is that, like the
bigstep evaluation relation for Imp, it is
deterministic.
Theorem: For each
t, there is at most one
t' such that
t
steps to
t' (
t ⇒ t' is provable). Formally, this is the
same as saying that
⇒ is deterministic.
Proof sketch: We show that if
x steps to both
y_{1} and
y_{2}, then
y_{1} and
y_{2} are equal, by induction on a derivation
of
step x y_{1}. There are several cases to consider, depending on
the last rule used in this derivation and the last rule in the
given derivation of
step x y_{2}.
 If both are ST_PlusConstConst, the result is immediate.
 The cases when both derivations end with ST_Plus1 or
ST_Plus2 follow by the induction hypothesis.
 It cannot happen that one is ST_PlusConstConst and the other
is ST_Plus1 or ST_Plus2, since this would imply that x
has the form P t_{1} t_{2} where both t_{1} and t_{2} are
constants (by ST_PlusConstConst) and one of t_{1} or t_{2}
has the form P _.
 Similarly, it cannot happen that one is ST_Plus1 and the
other is ST_Plus2, since this would imply that x has the
form P t_{1} t_{2} where t_{1} has both the form P t_{11} t_{12} and the
form C n. ☐
Formally:
Definition deterministic {
X:
Type} (
R:
relation X) :=
∀x y_{1} y_{2} :
X,
R x y_{1} → R x y_{2} → y_{1} =
y_{2}.
Module SimpleArith2.
Import SimpleArith1.
Theorem step_deterministic:
deterministic step.
Proof.
unfold deterministic.
intros x y_{1} y_{2} Hy_{1} Hy_{2}.
generalize dependent y_{2}.
induction Hy_{1};
intros y_{2} Hy_{2}.

inversion Hy_{2}.
+
reflexivity.
+
inversion H_{2}.
+
inversion H_{2}.

inversion Hy_{2}.
+
rewrite ← H_{0} in Hy_{1}.
inversion Hy_{1}.
+
rewrite ← (
IHHy1 t_{1}'0).
reflexivity.
assumption.
+
rewrite ← H in Hy_{1}.
inversion Hy_{1}.

inversion Hy_{2}.
+
rewrite ← H_{1} in Hy_{1}.
inversion Hy_{1}.
+
inversion H_{2}.
+
rewrite ← (
IHHy1 t_{2}'0).
reflexivity.
assumption.
Qed.
End SimpleArith2.
There is some annoying repetition in this proof. Each use of
inversion Hy_{2} results in three subcases, only one of which is
relevant (the one that matches the current case in the induction
on
Hy_{1}). The other two subcases need to be dismissed by finding
the contradiction among the hypotheses and doing inversion on it.
The following custom tactic, called
solve_by_inverts, can be
helpful in such cases. It will solve the goal if it can be solved
by inverting some hypothesis; otherwise, it fails.
Ltac solve_by_inverts n :=
match goal with 
H : ?
T ⊢ _ ⇒
match type of T with Prop ⇒
solve [
inversion H;
match n with S (
S (?
n')) ⇒
subst;
solve_by_inverts (
S n')
end ]
end end.
The details of how this works are not important for now, but it
illustrates the power of Coq's
Ltac language for
programmatically defining specialpurpose tactics. It looks
through the current proof state for a hypothesis
H (the first
match) of type
Prop (the second
match) such that performing
inversion on
H (followed by a recursive invocation of the same
tactic, if its argument
n is greater than one) completely solves
the current goal. If no such hypothesis exists, it fails.
We will usually want to call
solve_by_inverts with argument
1 (especially as larger arguments can lead to very slow proof
checking), so we define
solve_by_invert as a shorthand for this
case.
Ltac solve_by_invert :=
solve_by_inverts 1.
Let's see how a proof of the previous theorem can be simplified
using this tactic...
Module SimpleArith3.
Import SimpleArith1.
Theorem step_deterministic_alt:
deterministic step.
Proof.
intros x y_{1} y_{2} Hy_{1} Hy_{2}.
generalize dependent y_{2}.
induction Hy_{1};
intros y_{2} Hy_{2};
inversion Hy_{2};
subst;
try solve_by_invert.

reflexivity.

apply IHHy1 in H_{2}.
rewrite H_{2}.
reflexivity.

apply IHHy1 in H_{2}.
rewrite H_{2}.
reflexivity.
Qed.
End SimpleArith3.
Values
Next, it will be useful to slightly reformulate the
definition of singlestep reduction by stating it in terms of
"values."
It is useful to think of the
⇒ relation as defining an
abstract machine:
 At any moment, the state of the machine is a term.
 A step of the machine is an atomic unit of computation —
here, a single "add" operation.
 The halting states of the machine are ones where there is no
more computation to be done.
We can then execute a term
t as follows:
 Take t as the starting state of the machine.
 Repeatedly use the ⇒ relation to find a sequence of
machine states, starting with t, where each state steps to
the next.
 When no more reduction is possible, "read out" the final state
of the machine as the result of execution.
Intuitively, it is clear that the final states of the
machine are always terms of the form
C n for some
n.
We call such terms
values.
Having introduced the idea of values, we can use it in the
definition of the
⇒ relation to write
ST_Plus2 rule in a
slightly more elegant way:

(ST_PlusConstConst)


P (C n_{1}) (C n_{2}) ⇒ C (n_{1} + n_{2}) 

t_{1} ⇒ t_{1}' 
(ST_Plus1)


P t_{1} t_{2} ⇒ P t_{1}' t_{2} 

value v_{1} 

t_{2} ⇒ t_{2}' 
(ST_Plus2)


P v_{1} t_{2} ⇒ P v_{1} t_{2}' 

Again, the variable names here carry important information:
by convention,
v_{1} ranges only over values, while
t_{1} and
t_{2}
range over arbitrary terms. (Given this convention, the explicit
value hypothesis is arguably redundant. We'll keep it for now,
to maintain a close correspondence between the informal and Coq
versions of the rules, but later on we'll drop it in informal
rules for brevity.)
Here are the formal rules:
Exercise: 3 stars, recommended (redo_determinism)
As a sanity check on this change, let's reverify determinism.
Proof sketch: We must show that if
x steps to both
y_{1} and
y_{2}, then
y_{1} and
y_{2} are equal. Consider the final rules used
in the derivations of
step x y_{1} and
step x y_{2}.
 If both are ST_PlusConstConst, the result is immediate.
 It cannot happen that one is ST_PlusConstConst and the other
is ST_Plus1 or ST_Plus2, since this would imply that x has
the form P t_{1} t_{2} where both t_{1} and t_{2} are constants (by
ST_PlusConstConst) and one of t_{1} or t_{2} has the form P _.
 Similarly, it cannot happen that one is ST_Plus1 and the other
is ST_Plus2, since this would imply that x has the form P
t_{1} t_{2} where t_{1} both has the form P t_{11} t_{12} and is a
value (hence has the form C n).
 The cases when both derivations end with ST_Plus1 or
ST_Plus2 follow by the induction hypothesis. ☐
Most of this proof is the same as the one above. But to get
maximum benefit from the exercise you should try to write your
formal version from scratch and just use the earlier one if you
get stuck.
☐
Strong Progress and Normal Forms
The definition of singlestep reduction for our toy language
is fairly simple, but for a larger language it would be easy to
forget one of the rules and accidentally create a situation where
some term cannot take a step even though it has not been
completely reduced to a value. The following theorem shows that
we did not, in fact, make such a mistake here.
Theorem (
Strong Progress): If
t is a term, then either
t
is a value or else there exists a term
t' such that
t ⇒ t'.
Proof: By induction on
t.
 Suppose t = C n. Then t is a value.
 Suppose t = P t_{1} t_{2}, where (by the IH) t_{1} either is a value
or can step to some t_{1}', and where t_{2} is either a value or
can step to some t_{2}'. We must show P t_{1} t_{2} is either a value
or steps to some t'.
 If t_{1} and t_{2} are both values, then t can take a step, by
ST_PlusConstConst.
 If t_{1} is a value and t_{2} can take a step, then so can t,
by ST_Plus2.
 If t_{1} can take a step, then so can t, by ST_Plus1. ☐
Or, formally:
Theorem strong_progress :
∀t,
value t ∨ (
∃t',
t ⇒ t').
Proof.
induction t.

left.
apply v_const.

right.
inversion IHt1.
+
inversion IHt2.
*
inversion H.
inversion H_{0}.
∃(
C (
n +
n_{0})).
apply ST_PlusConstConst.
*
inversion H_{0} as [
t' H_{1}].
∃(
P t_{1} t').
apply ST_Plus2.
apply H.
apply H_{1}.
+
inversion H as [
t' H_{0}].
∃(
P t' t_{2}).
apply ST_Plus1.
apply H_{0}.
Qed.
This important property is called
strong progress, because
every term either is a value or can "make progress" by stepping to
some other term. (The qualifier "strong" distinguishes it from a
more refined version that we'll see in later chapters, called
just
progress.)
The idea of "making progress" can be extended to tell us something
interesting about values: in this language, values are exactly the
terms that
cannot make progress in this sense.
To state this observation formally, let's begin by giving a name
to terms that cannot make progress. We'll call them
normal
forms.
Note that this definition specifies what it is to be a normal form
for an
arbitrary relation
R over an arbitrary set
X, not
just for the particular singlestep reduction relation over terms
that we are interested in at the moment. We'll reuse the same
terminology for talking about other relations later in the
course.
We can use this terminology to generalize the observation we made
in the strong progress theorem: in this language, normal forms and
values are actually the same thing.
Why is this interesting?
Because
value is a syntactic concept — it is defined by looking
at the form of a term — while
normal_form is a semantic one —
it is defined by looking at how the term steps. It is not obvious
that these concepts should coincide! Indeed, we could easily have
written the definitions so that they would
not coincide.
Exercise: 3 stars, optional (value_not_same_as_normal_form)
We might, for example, mistakenly define
value so that it
includes some terms that are not finished reducing. (Even if you
don't work this exercise and the following ones in Coq, make sure
you can think of an example of such a term.)
☐
Exercise: 2 stars, optional (value_not_same_as_normal_form)
Alternatively, we might mistakenly define
step so that it
permits something designated as a value to reduce further.
☐
Exercise: 3 stars, optional (value_not_same_as_normal_form')
Finally, we might define
value and
step so that there is some
term that is not a value but that cannot take a step in the
step
relation. Such terms are said to be
stuck. In this case this is
caused by a mistake in the semantics, but we will also see
situations where, even in a correct language definition, it makes
sense to allow some terms to be stuck.
(Note that ST_Plus2 is missing.)
☐
Here is another very simple language whose terms, instead of being
just addition expressions and numbers, are just the booleans true
and false and a conditional expression...
Exercise: 1 star (smallstep_bools)
Which of the following propositions are provable? (This is just a
thought exercise, but for an extra challenge feel free to prove
your answers in Coq.)
☐
Exercise: 3 stars, optional (progress_bool)
Just as we proved a progress theorem for plus expressions, we can
do so for boolean expressions, as well.
☐
Exercise: 2 stars, optional (step_deterministic)
☐
Exercise: 2 stars (smallstep_bool_shortcut)
Suppose we want to add a "short circuit" to the step relation for
boolean expressions, so that it can recognize when the
then and
else branches of a conditional are the same value (either
ttrue or
tfalse) and reduce the whole conditional to this
value in a single step, even if the guard has not yet been reduced
to a value. For example, we would like this proposition to be
provable:
tif
(
tif ttrue ttrue ttrue)
tfalse
tfalse
⇒
tfalse.
Write an extra clause for the step relation that achieves this
effect and prove
bool_step_prop4.
☐
Exercise: 3 stars, optional (properties_of_altered_step)
It can be shown that the determinism and strong progress theorems
for the step relation in the lecture notes also hold for the
definition of step given above. After we add the clause
ST_ShortCircuit...
 Is the step relation still deterministic? Write yes or no and
briefly (1 sentence) explain your answer.
Optional: prove your answer correct in Coq.
 Does a strong progress theorem hold? Write yes or no and
briefly (1 sentence) explain your answer.
Optional: prove your answer correct in Coq.
 In general, is there any way we could cause strong progress to
fail if we took away one or more constructors from the original
step relation? Write yes or no and briefly (1 sentence) explain
your answer.
☐
MultiStep Reduction
We've been working so far with the
singlestep reduction
relation
⇒, which formalizes the individual steps of an
abstract machine for executing programs.
We can use the same machine to reduce programs to completion — to
find out what final result they yield. This can be formalized as
follows:
 First, we define a multistep reduction relation ⇒*, which
relates terms t and t' if t can reach t' by any number
(including zero) of single reduction steps.
 Then we define a "result" of a term t as a normal form that
t can reach by multistep reduction.
Since we'll want to reuse the idea of multistep reduction many
times, let's take a little extra trouble and define it
generically.
Given a relation
R, we define a relation
multi R, called the
multistep closure of R as follows.
(In the
Rel chapter and the Coq standard library, this relation
is called
clos_refl_trans_1n. We give it a shorter name here
for the sake of readability.)
The effect of this definition is that
multi R relates two
elements
x and
y if
 x = y, or
 R x y, or
 there is some nonempty sequence z_{1}, z_{2}, ..., zn such that
R x z_{1}
R z_{1} z_{2}
...
R zn y.
Thus, if
R describes a singlestep of computation, then
z_{1}...
zn
is the sequence of intermediate steps of computation between
x and
y.
We write
⇒* for the
multi step relation on terms.
Notation " t '
⇒*' t' " := (
multi step t t') (
at level 40).
The relation
multi R has several crucial properties.
First, it is obviously
reflexive (that is,
∀ x, multi R x
x). In the case of the
⇒* (i.e.,
multi step) relation, the
intuition is that a term can execute to itself by taking zero
steps of execution.
Second, it contains
R — that is, singlestep executions are a
particular case of multistep executions. (It is this fact that
justifies the word "closure" in the term "multistep closure of
R.")
Third, multi R is transitive.
In particular, for the multi step relation on terms, if
t_{1}⇒*t_{2} and t_{2}⇒*t_{3}, then t_{1}⇒*t_{3}.
Examples
Here's a specific instance of the
multi step relation:
Here's an alternate proof of the same fact that uses eapply to
avoid explicitly constructing all the intermediate terms.
Exercise: 1 star, optional (test_multistep_2)
☐
Exercise: 1 star, optional (test_multistep_3)
☐
Exercise: 2 stars (test_multistep_4)
☐
Normal Forms Again
If
t reduces to
t' in zero or more steps and
t' is a
normal form, we say that "
t' is a normal form of
t."
We have already seen that, for our language, singlestep reduction is
deterministic — i.e., a given term can take a single step in
at most one way. It follows from this that, if
t can reach
a normal form, then this normal form is unique. In other words, we
can actually pronounce
normal_form t t' as "
t' is
the
normal form of
t."
Exercise: 3 stars, optional (normal_forms_unique)
☐
Indeed, something stronger is true for this language (though not
for all languages): the reduction of
any term
t will
eventually reach a normal form — i.e.,
normal_form_of is a
total function. Formally, we say the
step relation is
normalizing.
To prove that
step is normalizing, we need a couple of lemmas.
First, we observe that, if
t reduces to
t' in many steps, then
the same sequence of reduction steps within
t is also possible
when
t appears as the lefthand child of a
P node, and
similarly when
t appears as the righthand child of a
P
node whose lefthand child is a value.
Exercise: 2 stars (multistep_congr_2)
☐
With these lemmas in hand, the main proof is a straightforward
induction.
Theorem: The
step function is normalizing — i.e., for every
t there exists some
t' such that
t steps to
t' and
t' is
a normal form.
Proof sketch: By induction on terms. There are two cases to
consider:
 t = C n for some n. Here t doesn't take a step, and we
have t' = t. We can derive the lefthand side by reflexivity
and the righthand side by observing (a) that values are normal
forms (by nf_same_as_value) and (b) that t is a value (by
v_const).
 t = P t_{1} t_{2} for some t_{1} and t_{2}. By the IH, t_{1} and t_{2}
have normal forms t_{1}' and t_{2}'. Recall that normal forms are
values (by nf_same_as_value); we know that t_{1}' = C n_{1} and
t_{2}' = C n_{2}, for some n_{1} and n_{2}. We can combine the ⇒*
derivations for t_{1} and t_{2} using multi_congr_1 and
multi_congr_1 to prove that P t_{1} t_{2} reduces in many steps to
C (n_{1} + n_{2}).
It is clear that our choice of t' = C (n_{1} + n_{2}) is a value,
which is in turn a normal form. ☐
Equivalence of BigStep Evaluation and SmallStep Reduction
Having defined the operational semantics of our tiny programming
language in two different ways (bigstep and smallstep), it makes
sense to ask whether these definitions actually define the same
thing! They do, though it takes a little work to show it. The
details are left as an exercise.
Exercise: 3 stars (eval__multistep)
The key ideas in the proof can be seen in the following picture:
P t_{1} t_{2} ⇒ (
by ST_Plus1)
P t_{1}' t_{2} ⇒ (
by ST_Plus1)
P t_{1}'' t_{2} ⇒ (
by ST_Plus1)
...
P (
C n_{1})
t_{2} ⇒ (
by ST_Plus2)
P (
C n_{1})
t_{2}' ⇒ (
by ST_Plus2)
P (
C n_{1})
t_{2}'' ⇒ (
by ST_Plus2)
...
P (
C n_{1}) (
C n_{2})
⇒ (
by ST_PlusConstConst)
C (
n_{1} +
n_{2})
That is, the multistep reduction of a term of the form
P t_{1} t_{2}
proceeds in three phases:
 First, we use ST_Plus1 some number of times to reduce t_{1}
to a normal form, which must (by nf_same_as_value) be a
term of the form C n_{1} for some n_{1}.
 Next, we use ST_Plus2 some number of times to reduce t_{2}
to a normal form, which must again be a term of the form C
n_{2} for some n_{2}.
 Finally, we use ST_PlusConstConst one time to reduce P (C
n_{1}) (C n_{2}) to C (n_{1} + n_{2}).
To formalize this intuition, you'll need to use the congruence
lemmas from above (you might want to review them now, so that
you'll be able to recognize when they are useful), plus some basic
properties of
⇒*: that it is reflexive, transitive, and
includes
⇒.
Proof.
Admitted.
☐
Exercise: 3 stars, advanced (eval__multistep_inf)
Write a detailed informal version of the proof of
eval__multistep.
☐
For the other direction, we need one lemma, which establishes a
relation between singlestep reduction and bigstep evaluation.
Exercise: 3 stars (step__eval)
Lemma step__eval :
∀t t' n,
t ⇒ t' →
t' ⇓ n →
t ⇓ n.
Proof.
intros t t' n Hs.
generalize dependent n.
Admitted.
☐
The fact that smallstep reduction implies bigstep evaluation is
now straightforward to prove, once it is stated correctly.
The proof proceeds by induction on the multistep reduction
sequence that is buried in the hypothesis
normal_form_of t t'.
Make sure you understand the statement before you start to
work on the proof.
Exercise: 3 stars (multistep__eval)
☐
Additional Exercises
Exercise: 3 stars, optional (interp_tm)
Remember that we also defined bigstep evaluation of terms as a
function
evalF. Prove that it is equivalent to the existing
semantics. (Hint: we just proved that
eval and
multistep are
equivalent, so logically it doesn't matter which you choose.
One will be easier than the other, though!)
☐
Exercise: 4 stars (combined_properties)
We've considered arithmetic and conditional expressions
separately. This exercise explores how the two interact.
Earlier, we separately proved for both plus and ifexpressions...
 that the step relation was deterministic, and
 a strong progress lemma, stating that every term is either a
value or can take a step.
Prove or disprove these two properties for the combined language.
☐
SmallStep Imp
Now for a more serious example: a smallstep version of the Imp
operational semantics.
The smallstep reduction relations for arithmetic and
boolean expressions are straightforward extensions of the tiny
language we've been working up to now. To make them easier to
read, we introduce the symbolic notations
⇒_{a} and
⇒_{b} for
the arithmetic and boolean step relations.
We are not actually going to bother to define boolean
values, since they aren't needed in the definition of ⇒_{b}
below (why?), though they might be if our language were a bit
larger (why?).
Reserved Notation " t '/' st '
⇒_{a}' t' " (
at level 40,
st at level 39).
Inductive astep :
state → aexp → aexp → Prop :=

AS_Id :
∀st i,
AId i /
st ⇒_{a} ANum (
st i)

AS_Plus :
∀st n_{1} n_{2},
APlus (
ANum n_{1}) (
ANum n_{2}) /
st ⇒_{a} ANum (
n_{1} +
n_{2})

AS_Plus1 :
∀st a_{1} a_{1}' a_{2},
a_{1} /
st ⇒_{a} a_{1}' →
(
APlus a_{1} a_{2}) /
st ⇒_{a} (
APlus a_{1}' a_{2})

AS_Plus2 :
∀st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} /
st ⇒_{a} a_{2}' →
(
APlus v_{1} a_{2}) /
st ⇒_{a} (
APlus v_{1} a_{2}')

AS_Minus :
∀st n_{1} n_{2},
(
AMinus (
ANum n_{1}) (
ANum n_{2})) /
st ⇒_{a} (
ANum (
minus n_{1} n_{2}))

AS_Minus1 :
∀st a_{1} a_{1}' a_{2},
a_{1} /
st ⇒_{a} a_{1}' →
(
AMinus a_{1} a_{2}) /
st ⇒_{a} (
AMinus a_{1}' a_{2})

AS_Minus2 :
∀st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} /
st ⇒_{a} a_{2}' →
(
AMinus v_{1} a_{2}) /
st ⇒_{a} (
AMinus v_{1} a_{2}')

AS_Mult :
∀st n_{1} n_{2},
(
AMult (
ANum n_{1}) (
ANum n_{2})) /
st ⇒_{a} (
ANum (
mult n_{1} n_{2}))

AS_Mult1 :
∀st a_{1} a_{1}' a_{2},
a_{1} /
st ⇒_{a} a_{1}' →
(
AMult (
a_{1}) (
a_{2})) /
st ⇒_{a} (
AMult (
a_{1}') (
a_{2}))

AS_Mult2 :
∀st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} /
st ⇒_{a} a_{2}' →
(
AMult v_{1} a_{2}) /
st ⇒_{a} (
AMult v_{1} a_{2}')
where " t '/' st '
⇒_{a}' t' " := (
astep st t t').
Reserved Notation " t '/' st '
⇒_{b}' t' " (
at level 40,
st at level 39).
Inductive bstep :
state → bexp → bexp → Prop :=

BS_Eq :
∀st n_{1} n_{2},
(
BEq (
ANum n_{1}) (
ANum n_{2})) /
st ⇒_{b}
(
if (
beq_nat n_{1} n_{2})
then BTrue else BFalse)

BS_Eq_{1} :
∀st a_{1} a_{1}' a_{2},
a_{1} /
st ⇒_{a} a_{1}' →
(
BEq a_{1} a_{2}) /
st ⇒_{b} (
BEq a_{1}' a_{2})

BS_Eq_{2} :
∀st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} /
st ⇒_{a} a_{2}' →
(
BEq v_{1} a_{2}) /
st ⇒_{b} (
BEq v_{1} a_{2}')

BS_LtEq :
∀st n_{1} n_{2},
(
BLe (
ANum n_{1}) (
ANum n_{2})) /
st ⇒_{b}
(
if (
leb n_{1} n_{2})
then BTrue else BFalse)

BS_LtEq1 :
∀st a_{1} a_{1}' a_{2},
a_{1} /
st ⇒_{a} a_{1}' →
(
BLe a_{1} a_{2}) /
st ⇒_{b} (
BLe a_{1}' a_{2})

BS_LtEq2 :
∀st v_{1} a_{2} a_{2}',
aval v_{1} →
a_{2} /
st ⇒_{a} a_{2}' →
(
BLe v_{1} a_{2}) /
st ⇒_{b} (
BLe v_{1} (
a_{2}'))

BS_NotTrue :
∀st,
(
BNot BTrue) /
st ⇒_{b} BFalse

BS_NotFalse :
∀st,
(
BNot BFalse) /
st ⇒_{b} BTrue

BS_NotStep :
∀st b_{1} b_{1}',
b_{1} /
st ⇒_{b} b_{1}' →
(
BNot b_{1}) /
st ⇒_{b} (
BNot b_{1}')

BS_AndTrueTrue :
∀st,
(
BAnd BTrue BTrue) /
st ⇒_{b} BTrue

BS_AndTrueFalse :
∀st,
(
BAnd BTrue BFalse) /
st ⇒_{b} BFalse

BS_AndFalse :
∀st b_{2},
(
BAnd BFalse b_{2}) /
st ⇒_{b} BFalse

BS_AndTrueStep :
∀st b_{2} b_{2}',
b_{2} /
st ⇒_{b} b_{2}' →
(
BAnd BTrue b_{2}) /
st ⇒_{b} (
BAnd BTrue b_{2}')

BS_AndStep :
∀st b_{1} b_{1}' b_{2},
b_{1} /
st ⇒_{b} b_{1}' →
(
BAnd b_{1} b_{2}) /
st ⇒_{b} (
BAnd b_{1}' b_{2})
where " t '/' st '
⇒_{b}' t' " := (
bstep st t t').
The semantics of commands is the interesting part. We need two
small tricks to make it work:
 We use SKIP as a "command value" — i.e., a command that
has reached a normal form.
 An assignment command reduces to SKIP (and an updated
state).
 The sequencing command waits until its lefthand
subcommand has reduced to SKIP, then throws it away so
that reduction can continue with the righthand
subcommand.
 We reduce a WHILE command by transforming it into a
conditional followed by the same WHILE.
(There are other ways of achieving the effect of the latter
trick, but they all share the feature that the original
WHILE
command needs to be saved somewhere while a single copy of the loop
body is being reduced.)
Reserved Notation " t '/' st '
⇒' t' '/' st' "
(
at level 40,
st at level 39,
t' at level 39).
Inductive cstep : (
com *
state)
→ (
com *
state)
→ Prop :=

CS_AssStep :
∀st i a a',
a /
st ⇒_{a} a' →
(
i ::=
a) /
st ⇒ (
i ::=
a') /
st

CS_Ass :
∀st i n,
(
i ::= (
ANum n)) /
st ⇒ SKIP / (
t_update st i n)

CS_SeqStep :
∀st c_{1} c_{1}' st' c_{2},
c_{1} /
st ⇒ c_{1}' /
st' →
(
c_{1} ;;
c_{2}) /
st ⇒ (
c_{1}' ;;
c_{2}) /
st'

CS_SeqFinish :
∀st c_{2},
(
SKIP ;;
c_{2}) /
st ⇒ c_{2} /
st

CS_IfTrue :
∀st c_{1} c_{2},
IFB BTrue THEN c_{1} ELSE c_{2} FI /
st ⇒ c_{1} /
st

CS_IfFalse :
∀st c_{1} c_{2},
IFB BFalse THEN c_{1} ELSE c_{2} FI /
st ⇒ c_{2} /
st

CS_IfStep :
∀st b b' c_{1} c_{2},
b /
st ⇒_{b} b' →
IFB b THEN c_{1} ELSE c_{2} FI /
st
⇒ (
IFB b' THEN c_{1} ELSE c_{2} FI) /
st

CS_While :
∀st b c_{1},
(
WHILE b DO c_{1} END) /
st
⇒ (
IFB b THEN (
c_{1};; (
WHILE b DO c_{1} END))
ELSE SKIP FI) /
st
where " t '/' st '
⇒' t' '/' st' " := (
cstep (
t,
st) (
t',
st')).
Concurrent Imp
Finally, to show the power of this definitional style, let's
enrich Imp with a new form of command that runs two subcommands in
parallel and terminates when both have terminated. To reflect the
unpredictability of scheduling, the actions of the subcommands may
be interleaved in any order, but they share the same memory and
can communicate by reading and writing the same variables.
Module CImp.
Inductive com :
Type :=

CSkip :
com

CAss :
id → aexp → com

CSeq :
com → com → com

CIf :
bexp → com → com → com

CWhile :
bexp → com → com

CPar :
com → com → com.
Notation "'SKIP'" :=
CSkip.
Notation "x '::=' a" :=
(
CAss x a) (
at level 60).
Notation "c
_{1} ;; c
_{2}" :=
(
CSeq c_{1} c_{2}) (
at level 80,
right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
(
CWhile b c) (
at level 80,
right associativity).
Notation "'IFB' b 'THEN' c
_{1} 'ELSE' c
_{2} 'FI'" :=
(
CIf b c_{1} c_{2}) (
at level 80,
right associativity).
Notation "'PAR' c
_{1} 'WITH' c
_{2} 'END'" :=
(
CPar c_{1} c_{2}) (
at level 80,
right associativity).
Inductive cstep : (
com *
state)
→ (
com *
state)
→ Prop :=

CS_AssStep :
∀st i a a',
a /
st ⇒_{a} a' →
(
i ::=
a) /
st ⇒ (
i ::=
a') /
st

CS_Ass :
∀st i n,
(
i ::= (
ANum n)) /
st ⇒ SKIP / (
t_update st i n)

CS_SeqStep :
∀st c_{1} c_{1}' st' c_{2},
c_{1} /
st ⇒ c_{1}' /
st' →
(
c_{1} ;;
c_{2}) /
st ⇒ (
c_{1}' ;;
c_{2}) /
st'

CS_SeqFinish :
∀st c_{2},
(
SKIP ;;
c_{2}) /
st ⇒ c_{2} /
st

CS_IfTrue :
∀st c_{1} c_{2},
(
IFB BTrue THEN c_{1} ELSE c_{2} FI) /
st ⇒ c_{1} /
st

CS_IfFalse :
∀st c_{1} c_{2},
(
IFB BFalse THEN c_{1} ELSE c_{2} FI) /
st ⇒ c_{2} /
st

CS_IfStep :
∀st b b' c_{1} c_{2},
b /
st ⇒_{b} b' →
(
IFB b THEN c_{1} ELSE c_{2} FI) /
st
⇒ (
IFB b' THEN c_{1} ELSE c_{2} FI) /
st

CS_While :
∀st b c_{1},
(
WHILE b DO c_{1} END) /
st
⇒ (
IFB b THEN (
c_{1};; (
WHILE b DO c_{1} END))
ELSE SKIP FI) /
st

CS_Par1 :
∀st c_{1} c_{1}' c_{2} st',
c_{1} /
st ⇒ c_{1}' /
st' →
(
PAR c_{1} WITH c_{2} END) /
st ⇒ (
PAR c_{1}' WITH c_{2} END) /
st'

CS_Par2 :
∀st c_{1} c_{2} c_{2}' st',
c_{2} /
st ⇒ c_{2}' /
st' →
(
PAR c_{1} WITH c_{2} END) /
st ⇒ (
PAR c_{1} WITH c_{2}' END) /
st'

CS_ParDone :
∀st,
(
PAR SKIP WITH SKIP END) /
st ⇒ SKIP /
st
where " t '/' st '
⇒' t' '/' st' " := (
cstep (
t,
st) (
t',
st')).
Definition cmultistep :=
multi cstep.
Notation " t '/' st '
⇒*' t' '/' st' " :=
(
multi cstep (
t,
st) (
t',
st'))
(
at level 40,
st at level 39,
t' at level 39).
Among the many interesting properties of this language is the fact
that the following program can terminate with the variable X set
to any value.
In particular, it can terminate with X set to 0:
It can also terminate with X set to 2:
More generally...
Exercise: 3 stars, optional
☐
Exercise: 3 stars, optional
☐
... the above loop can exit with
X having any value
whatsoever.
A SmallStep Stack Machine
Our last example is a smallstep semantics for the stack machine
example from the
Imp chapter.
Definition stack :=
list nat.
Definition prog :=
list sinstr.
Inductive stack_step :
state → prog *
stack → prog *
stack → Prop :=

SS_Push :
∀st stk n p',
stack_step st (
SPush n ::
p',
stk) (
p',
n ::
stk)

SS_Load :
∀st stk i p',
stack_step st (
SLoad i ::
p',
stk) (
p',
st i ::
stk)

SS_Plus :
∀st stk n m p',
stack_step st (
SPlus ::
p',
n::
m::
stk) (
p', (
m+
n)::
stk)

SS_Minus :
∀st stk n m p',
stack_step st (
SMinus ::
p',
n::
m::
stk) (
p', (
m
n)::
stk)

SS_Mult :
∀st stk n m p',
stack_step st (
SMult ::
p',
n::
m::
stk) (
p', (
m*
n)::
stk).
Theorem stack_step_deterministic :
∀st,
deterministic (
stack_step st).
Proof.
unfold deterministic.
intros st x y_{1} y_{2} H_{1} H_{2}.
induction H_{1};
inversion H_{2};
reflexivity.
Qed.
Definition stack_multistep st :=
multi (
stack_step st).
Exercise: 3 stars, advanced (compiler_is_correct)
Remember the definition of
compile for
aexp given in the
Imp chapter. We want now to prove
compile correct with respect
to the stack machine.
State what it means for the compiler to be correct according to
the stack machine small step semantics and then prove it.