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

Similarly, Hoare logic uses big-step semantics to talk about the relationship between the starting and final state (if any) of a program.

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 (* Constant *)
| P : tm → tm → tm. (* Plus *)

Big-step evaluation as a function

Fixpoint evalF (t : tm) : nat :=
  match t with
  | C n ⇒ n
  | P t₁ t₂ ⇒ evalF t₁ + evalF t₂
  end.

Big-step evaluation as a relation

	(E_Const)

C n ==> n

t₁ ==> n₁
t₂ ==> n₂	(E_Plus)

P t₁ t₂ ==> n₁ + n₂

Inductive eval : tm → nat → Prop :=
  | E_Const : ∀ n,
      C n ==> n
  | E_Plus : ∀ t₁ t₂ n₁ n₂,
      t₁ ==> n₁ →
      t₂ ==> n₂ →
      P t₁ t₂ ==> (n₁ + n₂)

Small-step evaluation relation

	(ST_PlusConstConst)

P (C n₁) (C n₂) --> C (n₁ + n₂)

t₁ --> t₁'	(ST_Plus1)

P t₁ t₂ --> P t₁' t₂

t₂ --> t₂'	(ST_Plus2)

P (C n₁) t₂ --> P (C n₁) t₂'

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 : ∀ n₁ n₂,
      P (C n₁) (C n₂) --> C (n₁ + n₂)
  | ST_Plus1 : ∀ t₁ t₁' t₂,
      t₁ --> t₁' →
      P t₁ t₂ --> P t₁' t₂
  | ST_Plus2 : ∀ n₁ t₂ t₂',
      t₂ --> t₂' →
      P (C n₁) t₂ --> P (C n₁) t₂'

Examples

If t₁ can take a step to t₁', then P t₁ t₂ steps to P t₁' t₂:

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 : ∀ n₁ n₂,
          P (C n₁) (C n₂) --> C (n₁ + n₂)
      | ST_Plus1 : ∀ t₁ t₁' t₂,
          t₁ --> t₁' →
          P t₁ t₂ --> P t₁' t₂
      | ST_Plus2 : ∀ n₁ t₂ t₂',
          t₂ --> t₂' →
          P (C n₁) t₂ --> P (C n₁) t₂'

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 : ∀ n₁ n₂,
          P (C n₁) (C n₂) --> C (n₁ + n₂)
      | ST_Plus1 : ∀ t₁ t₁' t₂,
          t₁ --> t₁' →
          P t₁ t₂ --> P t₁' t₂
      | ST_Plus2 : ∀ n₁ t₂ t₂',
          t₂ --> t₂' →
          P (C n₁) t₂ --> P (C n₁) t₂'

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 y₁ y₂ : X, R x y₁ → R x y₂ → y₁ = y₂.

Theorem step_deterministic:
deterministic step.

Proof.
  unfold deterministic. intros x y₁ y₂ Hy₁ Hy₂.
  generalize dependent y₂.
  induction Hy₁; intros y₂ Hy₂.
  - (* ST_PlusConstConst *) inversion Hy₂; subst.
    + (* ST_PlusConstConst *) reflexivity.
    + (* ST_Plus1 *) inversion H₂.
    + (* ST_Plus2 *) inversion H₂.
  - (* ST_Plus1 *) inversion Hy₂; subst.
    + (* ST_PlusConstConst *)
      inversion Hy₁.
    + (* ST_Plus1 *)
      apply IHHy1 in H₂. rewrite H₂. reflexivity.
    + (* ST_Plus2 *)
      inversion Hy₁.
  - (* ST_Plus2 *) inversion Hy₂; subst.
    + (* ST_PlusConstConst *)
      inversion Hy₁.
    + (* ST_Plus1 *) inversion H₂.
    + (* ST_Plus2 *)
      apply IHHy1 in H₂. rewrite H₂. reflexivity.
Qed.

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 y₁ y₂ Hy₁ Hy₂.
  generalize dependent y₂.
  induction Hy₁; intros y₂ Hy₂;
    inversion Hy₂; subst; try solve_by_invert.
  - (* ST_PlusConstConst *) reflexivity.
  - (* ST_Plus1 *)
    apply IHHy1 in H₂. rewrite H₂. reflexivity.
  - (* ST_Plus2 *)
    apply IHHy1 in H₂. rewrite H₂. 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 n₁) (C n₂) --> C (n₁ + n₂)

t₁ --> t₁'	(ST_Plus1)

P t₁ t₂ --> P t₁' t₂

value v₁
t₂ --> t₂'	(ST_Plus2)

P v₁ t₂ --> P v₁ t₂'

Again, variable names carry important information:

v₁ ranges only over values
t₁ and t₂ 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 : ∀ n₁ n₂,
          P (C n₁) (C n₂)
      --> C (n₁ + n₂)
  | ST_Plus1 : ∀ t₁ t₁' t₂,
        t₁ --> t₁' →
        P t₁ t₂ --> P t₁' t₂
  | ST_Plus2 : ∀ v₁ t₂ t₂',
        value v₁ → (* <--- n.b. *)
        t₂ --> t₂' →
        P v₁ t₂ --> P v₁ t₂'

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.
  - (* C *) left. apply v_const.
  - (* P *) right. destruct IHt1 as [IHt1 | [t₁' Ht₁] ].
    + (* l *) destruct IHt2 as [IHt2 | [t₂' Ht₂] ].
      × (* l *) inversion IHt1. inversion IHt2.
        ∃ (C (n + n₀)).
        apply ST_PlusConstConst.
      × (* r *)
        ∃ (P t₁ t₂').
        apply ST_Plus2. apply IHt1. apply Ht₂.
    + (* r *)
      ∃ (P t₁' t₂).
      apply ST_Plus1. apply Ht₁.
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, though not generally) 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. (* a corollary of strong_progress... *)
  unfold normal_form. intros t H.
  assert (G : value t ∨ ∃ t', t --> t').
  { apply strong_progress. }
  destruct G as [G | G].
  - (* l *) apply G.
  - (* r *) exfalso. apply H. assumption.
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 : ∀ t₁ n₂,
                value (P t₁ (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 : ∀ t₁ n₂,
                      value (P t₁ (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 : ∀ t₁ n₂,
                      value (P t₁ (C n₂)).

We obviously also 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.
(* FILL IN HERE *) 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). (* Original definition *)

Inductive step : tm → tm → Prop :=
  | ST_Funny : ∀ n,
      C n --> P (C n) (C 0) (* <--- NEW *)
  | ST_PlusConstConst : ∀ n₁ n₂,
      P (C n₁) (C n₂) --> C (n₁ + n₂)
  | ST_Plus1 : ∀ t₁ t₁' t₂,
      t₁ --> t₁' →
      P t₁ t₂ --> P t₁' t₂
  | ST_Plus2 : ∀ v₁ t₂ t₂',
      value v₁ →
      t₂ --> t₂' →
      P v₁ t₂ --> P v₁ t₂'

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 : ∀ n₁ n₂,
           P (C n₁) (C n₂) --> C (n₁ + n₂)
       | ST_Plus1 : ∀ t₁ t₁' t₂,
           t₁ --> t₁' →
           P t₁ t₂ --> P t₁' t₂
       | ST_Plus2 : ∀ v₁ t₂ t₂',
           value v₁ →
           t₂ --> t₂' →
           P v₁ t₂ --> P v₁ t₂'

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.
(* FILL IN HERE *) 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 : ∀ n₁ n₂,
      P (C n₁) (C n₂) --> C (n₁ + n₂)
  | ST_Plus1 : ∀ t₁ t₁' t₂,
      t₁ --> t₁' →
      P t₁ t₂ --> P t₁' t₂

(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 : ∀ n₁ n₂,
          P (C n₁) (C n₂) --> C (n₁ + n₂)
      | ST_Plus1 : ∀ t₁ t₁' t₂,
          t₁ --> t₁' →
          P t₁ t₂ --> P t₁' t₂

And, once again:

Lemma value_not_same_as_normal_form :
∃ t, ¬value t ∧ normal_form step t.

Proof.
(* FILL IN HERE *) 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 -->* to capture the intermediate results of a computation.

Since we'll want to reuse the idea of multi-step reduction many times, let's pause and define it generically.

Given a relation R (which will be --> for present purposes), we define a 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.

Full: (In the Rel chapter of Logical Foundations 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₁, z₂, ..., zn such that
           R x z₁
           R z₁ z₂
           ...
           R zn y.

Thus, if R describes a single-step of computation, then z₁ ... 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, single-step executions 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.
    - (* multi_refl *) assumption.
    - (* multi_step *)
      apply multi_step with y. assumption.
      apply IHG. assumption.
Qed.

In particular, for the multi step relation on terms, if t₁ -->* t₂ and t₂ -->* t₃, then t₁ -->* t₃.

Examples

Here's a specific instance of the multi step relation:

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 when the first argument is a value.

Lemma multistep_congr_1 : ∀ t₁ t₁' t₂,
t₁ -->* t₁' →
P t₁ t₂ -->* P t₁' t₂.

Proof.
  intros t₁ t₁' t₂ H. induction H.
  - (* multi_refl *) apply multi_refl.
  - (* multi_step *) apply multi_step with (P y t₂).
    + apply ST_Plus1. apply H.
    + apply IHmulti.
Qed.

Lemma multistep_congr_2 : ∀ t₁ t₂ t₂',
     value t₁ →
     t₂ -->* t₂' →
     P t₁ t₂ -->* P t₁ t₂'.

Proof.
(* FILL IN HERE *) Admitted.

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 reduces 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 left-hand side by reflexivity and the right-hand 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₁ t₂ for some t₁ and t₂. By the IH, t₁ and t₂ reduce to normal forms t₁' and t₂'. Recall that normal forms are values (by nf_same_as_value); we therefore know that t₁' = C n₁ and t₂' = C n₂, for some n₁ and n₂. We can combine the -->* derivations for t₁ and t₂ using multi_congr_1 and multi_congr_2 to prove that P t₁ t₂ reduces in many steps to t' = C (n₁ + n₂).

Finally, C (n₁ + n₂) is a value, which is in turn a normal form by nf_same_as_value. ☐

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!

Theorem eval__multistep : ∀ t n,
t ==> n → t -->* C n.

The key ideas in the proof can be seen in the following picture:
       P t₁ t₂ --> (by ST_Plus1)
       P t₁' t₂ --> (by ST_Plus1)
       P t₁'' t₂ --> (by ST_Plus1)
       ...
       P (C n₁) t₂ --> (by ST_Plus2)
       P (C n₁) t₂' --> (by ST_Plus2)
       P (C n₁) t₂'' --> (by ST_Plus2)
       ...
       P (C n₁) (C n₂) --> (by ST_PlusConstConst)
       C (n₁ + n₂) That is, the multistep reduction of a term of the form P t₁ t₂ proceeds in three phases:

First, we use ST_Plus1 some number of times to reduce t₁ to a normal form, which must (by nf_same_as_value) be a term of the form C n₁ for some n₁.
Next, we use ST_Plus2 some number of times to reduce t₂ to a normal form, which must again be a term of the form C n₂ for some n₂.
Finally, we use ST_PlusConstConst one time to reduce P (C n₁) (C n₂) to C (n₁ + n₂).

Proof.
(* FILL IN HERE *) Admitted.

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.
(* FILL IN HERE *) 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.
(* FILL IN HERE *) 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)

a₁ / st --> a₁'	(AS_Plus1)

a₁ + a₂ / st --> a₁' + a₂

aval v₁ a₂ / st --> a₂'	(AS_Plus2)

v₁ + a₂ / st --> v₁ + a₂'

	(AS_Plus)

n₁ + n₂ / st --> (n₁ + n₂)

a₁ / st --> a₁'	(AS_Minus1)

a₁ - a₂ / st --> a₁' - a₂

aval v₁ a₂ / st --> a₂'	(AS_Minus2)

v₁ - a₂ / st --> v₁ - a₂'

	(AS_Minus)

n₁ - n₂ / st --> (n₁ - n₂)

a₁ / st --> a₁'	(AS_Mult1)

a₁ * a₂ / st --> a₁' * a₂

aval v₁ a₂ / st --> a₂'	(AS_Mult2)

v₁ * a₂ / st --> v₁ * a₂'

	(AS_Mult)

n₁ * n₂ / st --> (n₁ * n₂)

In Coq

Reserved Notation " a '/' st '-->a' a' "
(at level 40, st at level 39).

Inductive astep (st : state) : aexp → aexp → Prop :=
  | AS_Id : ∀ (i : string),
      i / st -->a (st i)
  | AS_Plus1 : ∀ a₁ a₁' a₂,
      a₁ / st -->a a₁' →
      <{ a₁ + a₂ }> / st -->a <{ a₁' + a₂ }>
  | AS_Plus2 : ∀ v₁ a₂ a₂',
      aval v₁ →
      a₂ / st -->a a₂' →
      <{ v₁ + a₂ }> / st -->a <{ v₁ + a₂' }>
  | AS_Plus : ∀ (n₁ n₂ : nat),
      <{ n₁ + n₂ }> / st -->a (n₁ + n₂)
  | AS_Minus1 : ∀ a₁ a₁' a₂,
      a₁ / st -->a a₁' →
      <{ a₁ - a₂ }> / st -->a <{ a₁' - a₂ }>
  | AS_Minus2 : ∀ v₁ a₂ a₂',
      aval v₁ →
      a₂ / st -->a a₂' →
      <{ v₁ - a₂ }> / st -->a <{ v₁ - a₂' }>
  | AS_Minus : ∀ (n₁ n₂ : nat),
      <{ n₁ - n₂ }> / st -->a (n₁ - n₂)
  | AS_Mult1 : ∀ a₁ a₁' a₂,
      a₁ / st -->a a₁' →
      <{ a₁ × a₂ }> / st -->a <{ a₁' × a₂ }>
  | AS_Mult2 : ∀ v₁ a₂ a₂',
      aval v₁ →
      a₂ / st -->a a₂' →
      <{ v₁ × a₂ }> / st -->a <{ v₁ × a₂' }>
  | AS_Mult : ∀ (n₁ n₂ : nat),
      <{ n₁ × n₂ }> / st -->a (n₁ × n₂)

    where " a '/' st '-->a' a' " := (astep st a a').

Small-step evaluation relation for boolean expressions

a₁ / st --> a₁'	(BS_Eq₁)

a₁ = a₂ / st --> a₁' = a₂

aval v₁ a₂ / st --> a₂'	(BS_Eq₂)

v₁ = a₂ / st --> v₁ = a₂'

	(BS_Eq)

n₁ = n₂ / st --> (if (n₁ =? n₂) then true else false)

a₁ / st --> a₁'	(BS_LtEq1)

a₁ <= a₂ / st --> a₁' <= a₂

aval v₁ a₂ / st --> a₂'	(BS_LtEq2)

v₁ <= a₂ / st --> v₁ <= a₂'

	(BS_LtEq)

n₁ <= n₂ / st --> (if (n₁ <=? n₂) then true else false)

b₁ / st --> b₁'	(BS_NotStep)

~b₁ / st --> ~b₁'

	(BS_NotTrue)

~ true / st --> false

	(BS_NotFalse)

~ false / st --> true

b₁ / st --> b₁'	(BS_AndStep)

b₁ && b₂ / st --> b₁' && b₂

b₂ / st --> b₂'	(BS_AndTrueStep)

true && b₂ / st --> true && b₂'

	(BS_AndFalse)

false && b₂ / st --> false

	(BS_AndTrueTrue)

true && true / st --> true

	(BS_AndTrueFalse)

true && false / st --> false

In Coq

Reserved Notation " b '/' st '-->b' b' "
(at level 40, st at level 39).

Inductive bstep (st : state) : bexp → bexp → Prop :=
| BS_Eq₁ : ∀ a₁ a₁' a₂,
    a₁ / st -->a a₁' →
    <{ a₁ = a₂ }> / st -->b <{ a₁' = a₂ }>
| BS_Eq₂ : ∀ v₁ a₂ a₂',
    aval v₁ →
    a₂ / st -->a a₂' →
    <{ v₁ = a₂ }> / st -->b <{ v₁ = a₂' }>
| BS_Eq : ∀ (n₁ n₂ : nat),
    <{ n₁ = n₂ }> / st -->b
    (if (n₁ =? n₂) then <{ true }> else <{ false }>)
| BS_LtEq1 : ∀ a₁ a₁' a₂,
    a₁ / st -->a a₁' →
    <{ a₁ ≤ a₂ }> / st -->b <{ a₁' ≤ a₂ }>
| BS_LtEq2 : ∀ v₁ a₂ a₂',
    aval v₁ →
    a₂ / st -->a a₂' →
    <{ v₁ ≤ a₂ }> / st -->b <{ v₁ ≤ a₂' }>
| BS_LtEq : ∀ (n₁ n₂ : nat),
    <{ n₁ ≤ n₂ }> / st -->b
    (if (n₁ <=? n₂) then <{ true }> else <{ false }>)
| BS_NotStep : ∀ b₁ b₁',
    b₁ / st -->b b₁' →
    <{ ¬b₁ }> / st -->b <{ ¬b₁' }>
| BS_NotTrue : <{ ¬true }> / st -->b <{ false }>
| BS_NotFalse : <{ ¬false }> / st -->b <{ true }>
| BS_AndStep : ∀ b₁ b₁' b₂,
    b₁ / st -->b b₁' →
    <{ b₁ && b₂ }> / st -->b <{ b₁' && b₂ }>
| BS_AndTrueStep : ∀ b₂ b₂',
    b₂ / st -->b b₂' →
    <{ true && b₂ }> / st -->b <{ true && b₂' }>
| BS_AndFalse : ∀ b₂,
    <{ false && b₂ }> / st -->b <{ false }>
| BS_AndTrueTrue : <{ true && true }> / st -->b <{ true }>
| BS_AndTrueFalse : <{ true && false }> / st -->b <{ false }>

where " b '/' st '-->b' b' " := (bstep st b b').

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 by transforming it into a conditional followed by the same while.

Small-step evaluation relation for commands

a₁ / st --> a₁'	(CS_AsgnStep)

i := a₁ / st --> i := a₁' / st

	(CS_Asgn)

i := n / st --> skip / (i !-> n ; st)

c₁ / st --> c₁' / st'	(CS_SeqStep)

c₁ ; c₂ / st --> c₁' ; c₂ / st'

	(CS_SeqFinish)

skip ; c₂ / st --> c₂ / st

b₁ / st --> b₁'	(CS_IfStep)

if b₁ then c₁ else c₂ end / st -->
if b₁' then c₁ else c₂ end / st

	(CS_IfTrue)

if true then c₁ else c₂ end / st --> c₁ / st

	(CS_IfFalse)

if false then c₁ else c₂ end / st --> c₂ / st

	(CS_While)

while b₁ do c₁ end / st -->
if b₁ then (c₁; while b₁ do c₁ end) else skip end / st

In Coq

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_AsgnStep : ∀ st i a₁ a₁',
      a₁ / st -->a a₁' →
      <{ i := a₁ }> / st --> <{ i := a₁' }> / st
  | CS_Asgn : ∀ st i (n : nat),
      <{ i := n }> / st --> <{ skip }> / (i !-> n ; st)
  | CS_SeqStep : ∀ st c₁ c₁' st' c₂,
      c₁ / st --> c₁' / st' →
      <{ c₁ ; c₂ }> / st --> <{ c₁' ; c₂ }> / st'
  | CS_SeqFinish : ∀ st c₂,
      <{ skip ; c₂ }> / st --> c₂ / st
  | CS_IfStep : ∀ st b₁ b₁' c₁ c₂,
      b₁ / st -->b b₁' →
      <{ if b₁ then c₁ else c₂ end }> / st
      -->
      <{ if b₁' then c₁ else c₂ end }> / st
  | CS_IfTrue : ∀ st c₁ c₂,
      <{ if true then c₁ else c₂ end }> / st --> c₁ / st
  | CS_IfFalse : ∀ st c₁ c₂,
      <{ if false then c₁ else c₂ end }> / st --> c₂ / st
  | CS_While : ∀ st b₁ c₁,
      <{ while b₁ do c₁ end }> / st
      -->
      <{ if b₁ then c₁; while b₁ do c₁ end else skip end }> / st

  where " t '/' st '-->' t' '/' st' " := (cstep (t,st) (t',st')).

Concurrent Imp

Finally, let's define a concurrent extension of Imp, to show off the power of our new tools...

Notation "x || y" :=
         (CPar x y)
           (in custom com at level 90, right associativity).
Notation "'skip'" :=
         CSkip (in custom com at level 0).
Notation "x := y" :=
         (CAsgn x y)
            (in custom com at level 0, x constr at level 0,
             y at level 85, no associativity).
Notation "x ; y" :=
         (CSeq x y)
           (in custom com at level 90, right associativity).
Notation "'if' x 'then' y 'else' z 'end'" :=
         (CIf x y z)
           (in custom com at level 89, x at level 99,
            y at level 99, z at level 99).
Notation "'while' x 'do' y 'end'" :=
         (CWhile x y)
            (in custom com at level 89, x at level 99, y at level 99).

New small-step evaluation relation for commands

c₁ / st --> c₁' / st'	(CS_Par1)

c₁ \|\| c₂ / st --> c₁' \|\| c₂ / st'

c₂ / st --> c₂' / st'	(CS_Par2)

c₁ \|\| c₂ / st --> c₁ \|\| c₂' / st'

	(CS_ParDone)

skip \|\| skip / st --> skip / st

In Coq

Inductive cstep : (com × state) → (com × state) → Prop :=
    (* Old part: *)
  | CS_AsgnStep : ∀ st i a₁ a₁',
      a₁ / st -->a a₁' →
      <{ i := a₁ }> / st --> <{ i := a₁' }> / st
  | CS_Asgn : ∀ st i (n : nat),
      <{ i := n }> / st --> <{ skip }> / (i !-> n ; st)
  | CS_SeqStep : ∀ st c₁ c₁' st' c₂,
      c₁ / st --> c₁' / st' →
      <{ c₁ ; c₂ }> / st --> <{ c₁' ; c₂ }> / st'
  | CS_SeqFinish : ∀ st c₂,
      <{ skip ; c₂ }> / st --> c₂ / st
  | CS_IfStep : ∀ st b₁ b₁' c₁ c₂,
      b₁ / st -->b b₁' →
      <{ if b₁ then c₁ else c₂ end }> / st
      -->
      <{ if b₁' then c₁ else c₂ end }> / st
  | CS_IfTrue : ∀ st c₁ c₂,
      <{ if true then c₁ else c₂ end }> / st --> c₁ / st
  | CS_IfFalse : ∀ st c₁ c₂,
      <{ if false then c₁ else c₂ end }> / st --> c₂ / st
  | CS_While : ∀ st b₁ c₁,
      <{ while b₁ do c₁ end }> / st
      -->
      <{ if b₁ then c₁; while b₁ do c₁ end else skip end }> / st
    (* New part: *)
  | CS_Par1 : ∀ st c₁ c₁' c₂ st',
      c₁ / st --> c₁' / st' →
      <{ c₁ || c₂ }> / st --> <{ c₁' || c₂ }> / st'
  | CS_Par2 : ∀ st c₁ c₂ c₂' st',
      c₂ / st --> c₂' / st' →
      <{ c₁ || c₂ }> / st --> <{ c₁ || c₂' }> / st'
  | CS_ParDone : ∀ st,
      <{ skip || skip }> / 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).

Which state cannot be obtained as a result of executing the following program (from some 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 cannot be obtained as a result of executing the following program (from some 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 ≥ 1

(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) 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 }>.

In particular, it can terminate with X set to 0:

Example par_loop_example_0:
  ∃ st',
       par_loop / empty_st -->* <{skip}> / st'
    ∧ st' X = 0.

Proof.
  unfold par_loop.
  eexists. split.
  eapply multi_step. apply CS_Par1.
    apply CS_Asgn.
  eapply multi_step. apply CS_Par2. apply CS_While.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq₁. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq. simpl.
  eapply multi_step. apply CS_Par2. apply CS_IfFalse.
  eapply multi_step. apply CS_ParDone.
  eapply multi_refl.
  reflexivity.
Qed.

It can also terminate with X set to 2:

Example par_loop_example_2:
  ∃ st',
       par_loop / empty_st -->* <{skip}> / st'
    ∧ st' X = 2.

Proof.
  unfold par_loop.
  eexists. split.
  eapply multi_step. apply CS_Par2. apply CS_While.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq₁. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq. simpl.
  eapply multi_step. apply CS_Par2. apply CS_IfTrue.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_AsgnStep. apply AS_Plus1. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_AsgnStep. apply AS_Plus.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_Asgn.
  eapply multi_step. apply CS_Par2. apply CS_SeqFinish.

  eapply multi_step. apply CS_Par2. apply CS_While.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq₁. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq. simpl.
  eapply multi_step. apply CS_Par2. apply CS_IfTrue.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_AsgnStep. apply AS_Plus1. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_AsgnStep. apply AS_Plus.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_Asgn.

  eapply multi_step. apply CS_Par1. apply CS_Asgn.
  eapply multi_step. apply CS_Par2. apply CS_SeqFinish.
  eapply multi_step. apply CS_Par2. apply CS_While.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq₁. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq. simpl.
  eapply multi_step. apply CS_Par2. apply CS_IfFalse.
  eapply multi_step. apply CS_ParDone.
  eapply multi_refl.
  reflexivity. Qed.

Aside: A normalize Tactic

Proofs that one expression multisteps to another can be tedious...

Example step_example1 :
  (P (C 3) (P (C 3) (C 4)))
  -->* (C 10).
Proof.
  apply multi_step with (P (C 3) (C 7)).
    apply ST_Plus2.
      apply v_const.
      apply ST_PlusConstConst.
  apply multi_step with (C 10).
    apply ST_PlusConstConst.
  apply multi_refl.
Qed.

The proof repeatedly applies multi_step until the term reaches a normal form. Fortunately The sub-proofs for the intermediate steps are simple enough that auto, with appropriate hints, can solve them.

Hint Constructors step value : core.
Example step_example1' :
  (P (C 3) (P (C 3) (C 4)))
  -->* (C 10).
Proof.
  eapply multi_step. auto. simpl.
  eapply multi_step. auto. simpl.
  apply multi_refl.
Qed.

The following custom Tactic Notation definition captures this pattern. In addition, before each step, we print out the current goal, so that we can follow how the term is being reduced.

Tactic Notation "print_goal" :=
match goal with ⊢ ?x ⇒ idtac x end.

Tactic Notation "normalize" :=
  repeat (print_goal; eapply multi_step ;
            [ (eauto 10; fail) | (instantiate; simpl)]);
  apply multi_refl.

Example step_example1'' :
  (P (C 3) (P (C 3) (C 4)))
  -->* (C 10).
Proof.
  normalize.
  (* The print_goal in the normalize tactic shows
     a trace of how the expression reduced...
         (P (C 3) (P (C 3) (C 4)) -->* C 10)
         (P (C 3) (C 7) -->* C 10)
         (C 10 -->* C 10)
  *)
Qed.

The normalize tactic also provides a simple way to calculate the normal form of a term, by starting with a goal with an existentially bound variable.

Example step_example1''' : ∃ e',
  (P (C 3) (P (C 3) (C 4)))
  -->* e'.
Proof.
  eexists. normalize.
Qed.

This time, the trace is:
       (P (C 3) (P (C 3) (C 4)) -->* ?e')
       (P (C 3) (C 7) -->* ?e')
       (C 10 -->* ?e') where ?e' is the variable ``guessed'' by eapply.