SmallstepSmall-step Operational Semantics
Big-step Evaluation
Our semantics for Imp is written in the so-called
"big-step" style...
Evaluation rules take an expression (or command) to a final answer
"all in one step":
2 + 2 + 3 × 4 ==> 16
But big-step semantics makes it hard to talk about what
happens
along the way...
Small-step Evaluation
Small-step style: Alternatively, we can show how to "reduce"
an expression to a simpler form by performing a single step
of computation:
2 + 2 + 3 × 4
--> 2 + 2 + 12
--> 4 + 12
--> 16
Advantages of the small-step style include:
- Finer-grained "abstract machine", closer to real
implementations
- Extends smoothly to concurrent languages and languages
with other sorts of computational effects.
- Separates divergence (nontermination) from
stuckness (run-time error)
A Toy Language
The world's simplest programming language:
Inductive tm : Type :=
| C : nat → tm
| P : tm → tm → tm.
Big-step evaluation as a function
Fixpoint evalF (t : tm) : nat :=
match t with
| C n ⇒ n
| P t1 t2 ⇒ evalF t1 + evalF t2
end.
Big-step evaluation as a relation
| t1 ==> n1 |
|
| t2 ==> n2 |
(E_Plus)
|
|
| P t1 t2 ==> n1 + n2 |
|
Inductive eval : tm → nat → Prop :=
| E_Const : ∀ n,
C n ==> n
| E_Plus : ∀ t1 t2 n1 n2,
t1 ==> n1 →
t2 ==> n2 →
P t1 t2 ==> (n1 + n2)
Small-step evaluation relation
| |
(ST_PlusConstConst)
|
|
| P (C n1) (C n2) --> C (n1 + n2) |
|
| t1 --> t1' |
(ST_Plus1)
|
|
| P t1 t2 --> P t1' t2 |
|
| t2 --> t2' |
(ST_Plus2)
|
|
| P (C n1) t2 --> P (C n1) t2' |
|
Notice:
- each step reduces the leftmost P node that is ready to go
- first rule tells how to rewrite this node
- second and third rules tell where to find it
- constants are not related to anything -- i.e., they do not step
to anything
Small-step evaluation in Coq
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n1 n2,
P (C n1) (C n2) --> C (n1 + n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 --> t1' →
P t1 t2 --> P t1' t2
| ST_Plus2 : ∀ n1 t2 t2',
t2 --> t2' →
P (C n1) t2 --> P (C n1) t2'
Examples
If
t1 can take a step to
t1', then
P t1 t2 steps
to
P t1' t2:
Example test_step_1 :
P
(
P (
C 1) (
C 3))
(
P (
C 2) (
C 4))
-->
P
(
C 4)
(
P (
C 2) (
C 4)).
Proof.
apply ST_Plus1. apply ST_PlusConstConst. Qed.
What does the following term step to?
P (P (C 1) (C 2)) (P (C 1) (C 2))
(1)
C 6
(2)
P (C 3) (P (C 1) (C 2))
(3)
P (P (C 1) (C 2)) (C 3)
(4)
P (C 3) (C 3)
(5) None of the above
_________________________________________________
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n1 n2,
P (C n1) (C n2) --> C (n1 + n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 --> t1' →
P t1 t2 --> P t1' t2
| ST_Plus2 : ∀ n1 t2 t2',
t2 --> t2' →
P (C n1) t2 --> P (C n1) t2'
What about this one?
C 1
(1)
C 1
(2)
P (C 0) (C 1)
(3) None of the above
_________________________________________________
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n1 n2,
P (C n1) (C n2) --> C (n1 + n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 --> t1' →
P t1 t2 --> P t1' t2
| ST_Plus2 : ∀ n1 t2 t2',
t2 --> t2' →
P (C n1) t2 --> P (C n1) t2'
Relations
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.
Definition relation (X : Type) := X → X → Prop.
The step relation
--> is an example of a relation on
tm.
Determinism
One simple property of the
--> relation is that, like the
big-step 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:
Definition deterministic {X : Type} (R : relation X) :=
∀ x y1 y2 : X, R x y1 → R x y2 → y1 = y2.
Theorem step_deterministic:
deterministic step.
Proof.
unfold deterministic. intros x y1 y2 Hy1 Hy2.
generalize dependent y2.
induction Hy1; intros y2 Hy2.
- inversion Hy2; subst.
+ reflexivity.
+ inversion H2.
+ inversion H2.
- inversion Hy2; subst.
+
inversion Hy1.
+
apply IHHy1 in H2. rewrite H2. reflexivity.
+
inversion Hy1.
- inversion Hy2; subst.
+
inversion Hy1.
+ inversion H2.
+
apply IHHy1 in H2. rewrite H2. reflexivity.
Qed.
Automation digression...
Let's define a little tactic to decrease annoying repetition in
this proof:
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.
Ltac solve_by_invert :=
solve_by_inverts 1.
The proof of the previous theorem can now be simplified...
Theorem step_deterministic_alt: deterministic step.
Proof.
intros x y1 y2 Hy1 Hy2.
generalize dependent y2.
induction Hy1; intros y2 Hy2;
inversion Hy2; subst; try solve_by_invert.
- reflexivity.
-
apply IHHy1 in H2. rewrite H2. reflexivity.
-
apply IHHy1 in H2. rewrite H2. reflexivity.
Qed.
Values
It can be 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.
Final states of the machine are terms of the form
C n for some
n. We call such terms
values.
Inductive value : tm → Prop :=
| v_const : ∀ n, value (C n).
This gives a more elegant way of writing the
ST_Plus2 rule:
| |
(ST_PlusConstConst)
|
|
| P (C n1) (C n2) --> C (n1 + n2) |
|
| t1 --> t1' |
(ST_Plus1)
|
|
| P t1 t2 --> P t1' t2 |
|
| value v1 |
|
| t2 --> t2' |
(ST_Plus2)
|
|
| P v1 t2 --> P v1 t2' |
|
Again, variable names carry important information:
- v1 ranges only over values
- t1 and t2 range over arbitrary terms
So the
value hypothesis in the last rule is actually redundant
in the informal presentation: The naming convention tells us where
to add it when translating the informal rule to Coq. We'll keep
it for now, but in later chapters we'll elide it.
Here are the formal rules:
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n1 n2,
P (C n1) (C n2)
--> C (n1 + n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 --> t1' →
P t1 t2 --> P t1' t2
| ST_Plus2 : ∀ v1 t2 t2',
value v1 →
t2 --> t2' →
P v1 t2 --> P v1 t2'
Strong Progress and Normal Forms
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'.
Theorem strong_progress :
∀ t,
value t ∨ (
∃ t',
t --> t').
Proof.
induction t.
- left. apply v_const.
- right. destruct IHt1 as [IHt1 | [t1' Ht1] ].
+ destruct IHt2 as [IHt2 | [t2' Ht2] ].
× inversion IHt1. inversion IHt2.
∃ (C (n + n0)).
apply ST_PlusConstConst.
×
∃ (P t1 t2').
apply ST_Plus2; auto.
+
∃ (P t1' t2).
apply ST_Plus1. apply Ht1.
Qed.
Normal forms
The idea of "making progress" can be extended to tell us something
interesting about values: they 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.
Definition normal_form {X : Type}
(R : relation X) (t : X) : Prop :=
¬∃ t', R t t'.
Values vs. normal forms
In this language, normal forms and values coincide:
Lemma value_is_nf :
∀ v,
value v →
normal_form step v.
Proof.
unfold normal_form. intros v H. destruct H.
intros contra. destruct contra. inversion H.
Qed.
Lemma nf_is_value :
∀ t,
normal_form step t →
value t.
Proof.
unfold normal_form.
intros t H.
assert (
G :
value t ∨
∃ t',
t --> t').
{
apply strong_progress. }
destruct G as [
G |
G].
-
apply G.
-
contradiction.
Qed.
Corollary nf_same_as_value :
∀ t,
normal_form step t ↔
value t.
Proof.
split.
-
apply nf_is_value.
-
apply value_is_nf.
Qed.
Why is this interesting?
Because
value is a syntactic concept -- it is defined by looking
at the way a term is written -- 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 characterize the same
set of terms!
Indeed, we could easily have written the definitions (incorrectly)
so that they would
not coincide.
We might, for example, define
value so that it
includes some terms that are not finished reducing.
Inductive value : tm → Prop :=
| v_const : ∀ n, value (C n)
| v_funny : ∀ t1 n,
value (P t1 (C n)).
Using this wrong definition of
value, how many different values
does the following term
step to (in zero or more steps)?
P
(P (C 1) (C 2))
(C 3)
________________________________________
Inductive value : tm → Prop :=
| v_const : ∀ n, value (C n)
| v_funny : ∀ t1 n,
value (P t1 (C n)).
How many different terms does the following term step to
in one step?
P (P (C 1) (C 2)) (P (C 3) (C 4))
________________________________________
Inductive value : tm → Prop :=
| v_const : ∀ n, value (C n)
| v_funny : ∀ t1 n,
value (P t1 (C n)).
Lemma value_not_same_as_normal_form :
∃ v,
value v ∧ ¬
normal_form step v.
Proof.
Admitted.
Or we might (again, wrongly) define
step so that it permits
something designated as a value to reduce further.
Inductive value : tm → Prop :=
| v_const : ∀ n, value (C n).
Inductive step : tm → tm → Prop :=
| ST_Funny : ∀ n,
C n --> P (C n) (C 0)
| ST_PlusConstConst : ∀ n1 n2,
P (C n1) (C n2) --> C (n1 + n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 --> t1' →
P t1 t2 --> P t1' t2
| ST_Plus2 : ∀ v1 t2 t2',
value v1 →
t2 --> t2' →
P v1 t2 --> P v1 t2'
How many different terms does the following term step to (in
exactly one step)?
P (C 1) (C 3)
_______________________________________
Inductive step : tm → tm → Prop :=
| ST_Funny : ∀ n,
C n --> P (C n) (C 0)
| ST_PlusConstConst : ∀ n1 n2,
P (C n1) (C n2) --> C (n1 + n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 --> t1' →
P t1 t2 --> P t1' t2
| ST_Plus2 : ∀ v1 t2 t2',
value v1 →
t2 --> t2' →
P v1 t2 --> P v1 t2'
And we again lose the property that values are the same as
normal forms:
Lemma value_not_same_as_normal_form :
∃ v,
value v ∧ ¬
normal_form step v.
Proof.
Admitted.
Finally, we might define
value and
step so that there is some
term that is
not a value but that
also cannot take a step.
Such terms are said to be
stuck.
Inductive value : tm → Prop :=
| v_const : ∀ n, value (C n).
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n1 n2,
P (C n1) (C n2) --> C (n1 + n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 --> t1' →
P t1 t2 --> P t1' t2
(Note that ST_Plus2 is missing.)
How many terms does the following term step to (in one step)?
P (C 1) (P (C 1) (C 2))
_________________________________________
Inductive step : tm → tm → Prop :=
| ST_PlusConstConst : ∀ n1 n2,
P (C n1) (C n2) --> C (n1 + n2)
| ST_Plus1 : ∀ t1 t1' t2,
t1 --> t1' →
P t1 t2 --> P t1' t2
Lemma value_not_same_as_normal_form :
∃ t, ¬
value t ∧
normal_form step t.
Proof.
Admitted.
Multi-Step Reduction
We can now use the single-step relation and the concept of value
to formalize an entire
execution of the abstract machine.
First, we define a
multi-step reduction relation -->* that
relates a starting term to
every term that it can reach by
some number of reduction steps (including zero).
Since we'll want to reuse the idea of multi-step reduction many
times with many different single-step relations, let's pause and
define the concept generically.
Given a relation
R (e.g., the step relation
-->), we define a
new relation
multi R, called the
multi-step closure of R as
follows.
Inductive multi {X : Type} (R : relation X) : relation X :=
| multi_refl : ∀ (x : X), multi R x x
| multi_step : ∀ (x y z : X),
R x y →
multi R y z →
multi R x z.
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 z1, z2, ..., zn such that
R x z1
R z1 z2
...
R zn y.
Intuitively, if
R describes a single-step of computation, then
z1 ...
zn are the intermediate steps of computation that get
us from
x to
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 reduction.
Second, it contains
R -- that is, single-step reductions are a
particular case of multi-step executions. (It is this fact that
justifies the word "closure" in the term "multi-step closure of
R.")
Theorem multi_R :
∀ (
X :
Type) (
R :
relation X) (
x y :
X),
R x y → (
multi R)
x y.
Proof.
intros X R x y H.
apply multi_step with y.
- apply H.
- apply multi_refl.
Qed.
Third,
multi R is
transitive.
Theorem multi_trans :
∀ (
X :
Type) (
R :
relation X) (
x y z :
X),
multi R x y →
multi R y z →
multi R x z.
Proof.
intros X R x y z G H.
induction G.
- assumption.
-
apply multi_step with y.
+ assumption.
+ apply IHG. assumption.
Qed.
In particular, for the multi step relation on terms, if
t1 -->* t2 and t2 -->* t3, then t1 -->* t3.
Which of the following relations on numbers
cannot be expressed
as
multi R for some
R?
(1) less than or equal
(2) strictly less than
(3) equal
(4) none of the above
Lemma test_multistep_1:
P
(
P (
C 0) (
C 3))
(
P (
C 2) (
C 4))
-->*
C ((0 + 3) + (2 + 4)).
Proof.
apply multi_step with
(P (C (0 + 3))
(P (C 2) (C 4))).
{ apply ST_Plus1. apply ST_PlusConstConst. }
apply multi_step with
(P (C (0 + 3))
(C (2 + 4))).
{ apply ST_Plus2.
- apply v_const.
- apply ST_PlusConstConst. }
apply multi_R.
apply ST_PlusConstConst.
Qed.
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."
Definition step_normal_form := normal_form step.
Definition normal_form_of (t t' : tm) :=
(t -->* t' ∧ step_normal_form t').
Notice:
- single-step reduction is deterministic;
- so, if t can reach a normal form, then this normal form is unique;
- so we can pronounce normal_form t t' as "t' is the
normal form of t."
Indeed, something stronger is true for this language:
- the reduction of any term t will eventually reach a
normal form
We say the
step relation is
normalizing.
Definition normalizing {X : Type} (R : relation X) :=
∀ t, ∃ t',
(multi R) t t' ∧ normal_form R t'.
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 first argument to
P, and
similarly when
t appears as the second argument to
P
(and the first argument is a value).
Lemma multistep_congr_1 :
∀ t1 t1' t2,
t1 -->* t1' →
P t1 t2 -->* P t1' t2.
Proof.
intros t1 t1' t2 H. induction H.
- apply multi_refl.
- apply multi_step with (P y t2).
+ apply ST_Plus1. apply H.
+ apply IHmulti.
Qed.
Lemma multistep_congr_2 :
∀ v1 t2 t2',
value v1 →
t2 -->* t2' →
P v1 t2 -->* P v1 t2'.
Proof.
Admitted.
Theorem step_normalizing :
normalizing step.
Proof.
unfold normalizing.
induction t.
-
∃ (C n).
split.
+ apply multi_refl.
+
apply nf_same_as_value. apply v_const.
-
destruct IHt1 as [t1' [Hsteps1 Hnormal1] ].
destruct IHt2 as [t2' [Hsteps2 Hnormal2] ].
apply nf_same_as_value in Hnormal1.
apply nf_same_as_value in Hnormal2.
destruct Hnormal1 as [n1].
destruct Hnormal2 as [n2].
∃ (C (n1 + n2)).
split.
+
apply multi_trans with (P (C n1) t2).
× apply multistep_congr_1. apply Hsteps1.
× apply multi_trans with (P (C n1) (C n2)).
{ apply multistep_congr_2.
- apply v_const.
- apply Hsteps2. }
apply multi_R. apply ST_PlusConstConst.
+
apply nf_same_as_value. apply v_const.
Qed.
Equivalence of Big-Step and Small-Step
Having defined the operational semantics of our tiny programming
language in two different ways (big-step and small-step), it makes
sense to ask whether these definitions actually define the same
thing!
We consider the two implications separately.
Theorem eval__multistep : ∀ t n,
t ==> n → t -->* C n.
The key ideas in the proof can be seen in the following picture:
P t1 t2 --> (by ST_Plus1)
P t1' t2 --> (by ST_Plus1)
P t1'' t2 --> (by ST_Plus1)
...
P (C v1) t2 --> (by ST_Plus2)
P (C v1) t2' --> (by ST_Plus2)
P (C v1) t2'' --> (by ST_Plus2)
...
P (C v1) (C v2) --> (by ST_PlusConstConst)
C (v1 + v2)
That is, the multistep reduction of a term of the form
P t1 t2
proceeds in three phases:
- First, we use ST_Plus1 some number of times to reduce t1
to a normal form, which must (by nf_same_as_value) be a
term of the form C v1 for some v1.
- Next, we use ST_Plus2 some number of times to reduce t2
to a normal form, which must again be a term of the form C
v2 for some v2.
- Finally, we use ST_PlusConstConst one time to reduce P (C
v1) (C v2) to C (v1 + v2).
For the other direction, we need one lemma, which establishes a
relation between single-step reduction and big-step evaluation.
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 small-step reduction implies big-step evaluation is now
straightforward to prove.
The proof proceeds by induction on the multi-step reduction
sequence that is buried in the hypothesis
normal_form_of t t'.
Theorem multistep__eval :
∀ t t',
normal_form_of t t' →
∃ n,
t' =
C n ∧
t ==>
n.
Proof.
Admitted.
Small-Step Imp
Now for a more serious example: a small-step version of the Imp
operational semantics.
Inductive aval : aexp → Prop :=
| av_num : ∀ n, aval (ANum n).
Small-step evaluation relation for arithmetic expressions
| |
(AS_Id)
|
|
| i / st --> (st i) |
|
| a1 / st --> a1' |
(AS_Plus1)
|
|
| a1 + a2 / st --> a1' + a2 |
|
| aval v1 a2 / st --> a2' |
(AS_Plus2)
|
|
| v1 + a2 / st --> v1 + a2' |
|
| |
(AS_Plus)
|
|
| v1 + v2 / st --> (v1 + v2) |
|
| a1 / st --> a1' |
(AS_Minus1)
|
|
| a1 - a2 / st --> a1' - a2 |
|
| aval v1 a2 / st --> a2' |
(AS_Minus2)
|
|
| v1 - a2 / st --> v1 - a2' |
|
| |
(AS_Minus)
|
|
| v1 - v2 / st --> (v1 - v2) |
|
| a1 / st --> a1' |
(AS_Mult1)
|
|
| a1 * a2 / st --> a1' * a2 |
|
| aval v1 a2 / st --> a2' |
(AS_Mult2)
|
|
| v1 * a2 / st --> v1 * a2' |
|
| |
(AS_Mult)
|
|
| v1 * v2 / st --> (v1 * v2) |
|
Small-step evaluation relation for boolean expressions
| a1 / st --> a1' |
(BS_Eq1)
|
|
| a1 = a2 / st --> a1' = a2 |
|
| aval v1 a2 / st --> a2' |
(BS_Eq2)
|
|
| v1 = a2 / st --> v1 = a2' |
|
| |
(BS_Eq)
|
|
| v1 = v2 / st --> (if (v1 =? v2) then true else false) |
|
| a1 / st --> a1' |
(BS_LtEq1)
|
|
| a1 <= a2 / st --> a1' <= a2 |
|
| aval v1 a2 / st --> a2' |
(BS_LtEq2)
|
|
| v1 <= a2 / st --> v1 <= a2' |
|
| |
(BS_LtEq)
|
|
| v1 <= v2 / st --> (if (v1 <=? v2) then true else false) |
|
| b1 / st --> b1' |
(BS_NotStep)
|
|
| ~b1 / st --> ~b1' |
|
| |
(BS_NotTrue)
|
|
| ~ true / st --> false |
|
| |
(BS_NotFalse)
|
|
| ~ false / st --> true |
|
| b1 / st --> b1' |
(BS_AndStep)
|
|
| b1 && b2 / st --> b1' && b2 |
|
| b2 / st --> b2' |
(BS_AndTrueStep)
|
|
| true && b2 / st --> true && b2' |
|
| |
(BS_AndFalse)
|
|
| false && b2 / st --> false |
|
| |
(BS_AndTrueTrue)
|
|
| true && true / st --> true |
|
| |
(BS_AndTrueFalse)
|
|
| true && false / st --> false |
|
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 left-hand
subcommand has reduced to skip, then throws it away so
that reduction can continue with the right-hand
subcommand.
- We reduce a while command a single step by transforming it
into a conditional followed by the same while.
Small-step evaluation relation for commands
| a1 / st --> a1' |
(CS_AsgnStep)
|
|
| i := a1 / st --> i := a1' / st |
|
| |
(CS_Asgn)
|
|
| i := n / st --> skip / (i !-> n ; st) |
|
| c1 / st --> c1' / st' |
(CS_SeqStep)
|
|
| c1 ; c2 / st --> c1' ; c2 / st' |
|
| |
(CS_SeqFinish)
|
|
| skip ; c2 / st --> c2 / st |
|
| b1 / st --> b1' |
(CS_IfStep)
|
|
| if b1 then c1 else c2 end / st --> |
|
| if b1' then c1 else c2 end / st |
|
| |
(CS_IfTrue)
|
|
| if true then c1 else c2 end / st --> c1 / st |
|
| |
(CS_IfFalse)
|
|
| if false then c1 else c2 end / st --> c2 / st |
|
| |
(CS_While)
|
|
| while b1 do c1 end / st --> |
|
| if b1 then (c1; while b1 do c1 end) else skip end / st |
|
Concurrent Imp
Finally, let's define a
concurrent extension of Imp, to
show off the power of our new tools...
For example:
- This program sets X to 0 in one thread and 1 in another,
leaving it set to either 0 or 1 at the end:
X := 0 || X := 1
- This one leaves X set to one of 0, 1, 2, or 3 at the
end:
X := 0; (X := X+2 || X := X+1 || X := 0)
Inductive com : Type :=
| CSkip : com
| CAsgn : string → aexp → com
| CSeq : com → com → com
| CIf : bexp → com → com → com
| CWhile : bexp → com → com
| CPar : com → com → com.
New small-step evaluation relation for commands
Same rules as before, plus:
| c1 / st --> c1' / st' |
(CS_Par1)
|
|
| c1 || c2 / st --> c1' || c2 / st' |
|
| c2 / st --> c2' / st' |
(CS_Par2)
|
|
| c1 || c2 / st --> c1 || c2' / st' |
|
| |
(CS_ParDone)
|
|
| skip || skip / st --> skip / 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).
Which state
cannot be obtained as a result of executing the
following program (from any starting state)?
(Y := 1 || Y := 2);
X := Y
(1)
Y=0 and
X=0
(2)
Y=1 and
X=1
(3)
Y=2 and
X=2
(4) None of the above
Which state(s)
cannot be obtained as a result of executing the
following program (from any starting state)?
(Y := 1 || Y := Y + 1);
X := Y
(1)
Y=1 and
X=1
(2)
Y=0 and
X=1
(3)
Y=2 and
X=2
(4)
Y=n and
X=n for any
n ≥ 3
(5) 2 and 4 above
(6) None of the above
How about this one?
( Y := 0; X := Y + 1 )
||
( Y := Y + 1; X := 1 )
(1)
Y=0 and
X=1
(2)
Y=1 and
X=1
(3)
Y=0 and
X=0
(4)
Y=4 and
X=1
(5) None of the above
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.
Definition par_loop : com :=
<{
Y := 1
||
while (Y = 0) do X := X + 1 end
}>.
