SmallstepSmall-step Operational Semantics
(* $Date: 2011-05-07 16:41:12 -0400 (Sat, 07 May 2011) $ *)
Require Export Imp.
Require Import Relations.
The evaluators we have seen so far (e.g., the ones for aexps,
bexps, and commands) have been formulated in a "big-step"
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 its use, 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 big-step style is more technical, but
critical for some applications. Consider the variant of Imp with
lists that we introduced in ImpList.v. We chose to define the
meaning of programs like 0 + nil by specifying that a list
should be interpreted as 0 when it occurs in a context expecting
a number, but this was a bit of a hack. It would be better simply
to say that the behavior of such a program is undefined — it
doesn't evaluate to any result. We could easily do this: we'd
just have to use the formulations of aeval and beval as
inductive propositions (rather than Fixpoints), so that we can
make them partial functions instead of total ones.
However, this way of defining Imp has 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 taking the successor of a boolean variable, and
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
different 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 finer-grained way of
defining and reasoning about program behaviors. This is the topic
of the present chapter. We replace the "big-step" eval relation
with a "small-step" relation that specifies, for a given program,
how the "atomic steps" of computation are performed.
To save space in the discussion, let's go back to an
incredibly simple language containing just constants and addition.
At the end of the chapter, we'll see how to apply the same
techniques to the full Imp language.
A Toy Language
Inductive tm : Type :=
| tm_const : nat → tm
| tm_plus : tm → tm → tm.
Tactic Notation "tm_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "tm_const" | Case_aux c "tm_plus" ].
Module SimpleArith0.
Here is a standard evaluator for this language, written in the
same (big-step) style as we've been using up to this point.
Fixpoint eval (t : tm) : nat :=
match t with
| tm_const n => n
| tm_plus a1 a2 => eval a1 + eval a2
end.
End SimpleArith0.
Module SimpleArith1.
Now, 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."
We write plus n1 n2 in the second rule, rather than n1 + n2,
to emphasize the fact that the + on the left of the ⇓ is an
abstract-syntax-tree node while the addition on the right of the
⇓ is the mathematical sum of the numbers n1 and n2. The
formal Coq version of the definition is more pedantic about this
distinction:
(E_Const) | |
n ⇓ n |
t1 ⇓ n1 | |
t2 ⇓ n2 | (E_Plus) |
t1 + t2 ⇓ plus n1 n2 |
Reserved Notation " t '⇓' n " (at level 50, left associativity).
Inductive eval : tm → nat → Prop :=
| E_Const : ∀ n,
tm_const n ⇓ n
| E_Plus : ∀ t1 t2 n1 n2,
t1 ⇓ n1 →
t2 ⇓ n2 →
tm_plus t1 t2 ⇓ plus n1 n2
where " t '⇓' n " := (eval t n).
End SimpleArith1.
Here is a slight variation, still in big-step style, where
the final result of evaluating a term is also a term, rather than
a bare number.
Reserved Notation " t '⇓' t' " (at level 50, left associativity).
Inductive eval : tm → tm → Prop :=
| E_Const : ∀ n1,
tm_const n1 ⇓ tm_const n1
| E_Plus : ∀ t1 n1 t2 n2,
t1 ⇓ tm_const n1 →
t2 ⇓ tm_const n2 →
tm_plus t1 t2 ⇓ tm_const (plus n1 n2)
where " t '⇓' t' " := (eval t t').
(Note that this doesn't change anything in the informal rules,
where we are eliding the distinction between the constant term
n and the bare number n.)
Tactic Notation "eval_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "E_Const" | Case_aux c "E_Plus" ].
Module SimpleArith2.
Now, here is a small-step version.
Note that we're using variable names here to lighten the notation:
by convention, n1 and n2 refer only to constants (constructed
with tm_const), while t1 and t2 refer to arbitrary terms.
In the formal rules, we use explicit constructors to make the same
distinction.
(ST_PlusConstConst) | |
n1 + n2 ⇒ plus n1 n2 |
t1 ⇓ t1' | (ST_Plus1) |
t1 + t2 ⇓ t1' + t2 |
t2 ⇓ t2' | (ST_Plus2) |
n1 + t2 ⇓ n1 + t2' |
Reserved Notation " t '⇒' t' " (at level 40).
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n1 n2,
tm_plus (tm_const n1) (tm_const n2) ⇒ tm_const (plus n1 n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 ⇒ t1' →
tm_plus t1 t2 ⇒ tm_plus t1' t2
| ST_Plus2 : ∀ n1 t2 t2',
t2 ⇒ t2' →
tm_plus (tm_const n1) t2 ⇒ tm_plus (tm_const n1) t2'
where " t '⇒' t' " := (step t t').
Things to notice:
- We are defining just a single reduction step, in which
one tm_plus node is replaced by its value.
- Each step finds the leftmost tm_plus 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 tm_plus node
itself; the other two rules tell how to find it.
- A term that is just a constant cannot take a step.
Tactic Notation "step_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "ST_PlusConstConst"
| Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].
A couple of examples of reasoning with the step
relation...
If t1 can take a step to t1', then tm_plus t1 t2 steps
to plus t1' t2:
Example test_step_1 :
tm_plus
(tm_plus (tm_const 0) (tm_const 3))
(tm_plus (tm_const 2) (tm_const 4))
⇒
tm_plus
(tm_const (plus 0 3))
(tm_plus (tm_const 2) (tm_const 4)).
Proof.
apply ST_Plus1. apply ST_PlusConstConst. Qed.
Exercise: 2 stars (test_step_2)
Right-hand sides of sums can take a step only when the left-hand side is finished: if t2 can take a step to t2', then tm_plus (tm_const n) t2 steps to tm_plus (tm_const n) t2':Example test_step_2 :
tm_plus
(tm_const 0)
(tm_plus
(tm_const 2)
(tm_plus (tm_const 0) (tm_const 3)))
⇒
tm_plus
(tm_const 0)
(tm_plus
(tm_const 2)
(tm_const (plus 0 3))).
Proof.
(* FILL IN HERE *) Admitted.
☐
One interesting property of the ⇒ relation is that, like the
evaluation relation for our language of Imp programs, 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 a partial function.
Proof sketch: We show that if x steps to both y1 and y2
then y1 and y2 are equal, by induction on a derivation of
step x y1. There are several cases to consider, depending on
the last rule used in this derivation and in the given derivation
of step x y2.
- 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 tm_plus t1 t2 where both t1 and t2 are
constants (by ST_PlusConstConst) and one of t1 or t2 has
the form tm_plus ....
- Similarly, it cannot happen that one is ST_Plus1 and the other is ST_Plus2, since this would imply that x has the form tm_plus t1 t2 where t1 has both the form tm_plus t1 t2 and the form tm_const n. ☐
Theorem step_deterministic:
partial_function step.
Proof.
unfold partial_function. intros x y1 y2 Hy1 Hy2.
generalize dependent y2.
step_cases (induction Hy1) Case; intros y2 Hy2.
Case "ST_PlusConstConst". step_cases (inversion Hy2) SCase.
SCase "ST_PlusConstConst". reflexivity.
SCase "ST_Plus1". inversion H2.
SCase "ST_Plus2". inversion H2.
Case "ST_Plus1". step_cases (inversion Hy2) SCase.
SCase "ST_PlusConstConst". rewrite ← H0 in Hy1. inversion Hy1.
SCase "ST_Plus1".
rewrite ← (IHHy1 t1'0).
reflexivity. assumption.
SCase "ST_Plus2". rewrite ← H in Hy1. inversion Hy1.
Case "ST_Plus2". step_cases (inversion Hy2) SCase.
SCase "ST_PlusConstConst". rewrite ← H1 in Hy1. inversion Hy1.
SCase "ST_Plus1". inversion H2.
SCase "ST_Plus2".
rewrite ← (IHHy1 t2'0).
reflexivity. assumption. Qed.
End SimpleArith2.
Values
- 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.
- 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.
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 intuitive way:
Again, the variable names here carry important information:
by convention, v1 ranges only over values, while t1 and t2
range over arbitrary terms. In the Coq version of the rules, we
use an explicit value hypothesis for the same purpose.
(ST_PlusConstConst) | |
n1 + n2 ⇒ plus n1 n2 |
t1 ⇓ t1' | (ST_Plus1) |
t1 + t2 ⇓ t1' + t2 |
t2 ⇓ t2' | (ST_Plus2) |
v1 + t2 ⇓ v1 + t2' |
Reserved Notation " t '⇒' t' " (at level 40).
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n1 n2,
tm_plus (tm_const n1) (tm_const n2)
⇒ tm_const (plus n1 n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 ⇒ t1' →
tm_plus t1 t2 ⇒ tm_plus t1' t2
| ST_Plus2 : ∀ v1 t2 t2',
value v1 → (* <----- n.b. *)
t2 ⇒ t2' →
tm_plus v1 t2 ⇒ tm_plus v1 t2'
where " t '⇒' t' " := (step t t').
Tactic Notation "step_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "ST_PlusConstConst"
| Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].
Exercise: 3 stars, recommended (redo_determinacy)
As a sanity check on this change, let's re-verify determinacy- 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 tm_plus t1 t2 where both t1 and t2 are
constants (by ST_PlusConstConst) AND one of t1 or t2 has
the form tm_plus ....
- Similarly, it cannot happen that one is ST_Plus1 and the other
is ST_Plus2, since this would imply that x has the form
tm_plus t1 t2 where t1 both has the form tm_plus t1 t2 and
is a value (hence has the form tm_const n).
- The cases when both derivations end with ST_Plus1 or ST_Plus2 follow by the induction hypothesis. ☐
☐