Problem Set 3

In class we saw a relational small-step semantics for IMP. Abhishek observed that the small-step semantics could be written as a function instead, since there is no recursion in the 'while' case. (However, there is a loss of extensibility to some nondeterministic features like concurrency.) Are these semantics really equivalent?

Here is the relational semantics we saw in class:

Inductive step_com : com -> state -> com -> state -> Prop :=
| Step_assign: forall s x e,
       step_com (Assign x e) s
                (Skip) (set x (eval_aexp e s) s)
| Step_seqL: forall c1 c2 c1' s s', step_com c1 s c1' s' ->
                step_com (Seq c1 c2) s (Seq c1' c2) s'
| Step_seqR: forall c s, step_com (Seq Skip c) s c s
| Step_if_true: forall b c1 c2 s, eval_bexp b s = true ->
                 step_com (If b c1 c2) s c1 s
| Step_if_false: forall b c1 c2 s, eval_bexp b s = false ->
                 step_com (If b c1 c2) s c2 s
| Step_while: forall b c s,
                 step_com (While b c) s
                          (If b (Seq c (While b c)) Skip) s.

1. Give a definition of the same small-step semantics, as a function.

Note that a final configuration should step to None.

Variable step_com_fn : com -> state -> option (com * state)

^^^ replace me ^^^

2. Prove that only Skip fails to step:

Lemma progress : forall c s, step_com_fn c s = None -> c = Skip.
Admitted.

3. Prove that all steps in the functional semantics work in the relational one.

Hints:

You will need to use induction, and you will need to use it at the right level of quantifier nesting in order to have a strong enough induction hypothesis.
Try doing the Seq case early to work out the inductive step. Some of the other cases will be doable in a specialized way, but everything other than Skip can be handled uniformly.
some handy tactics to try: discriminate, congruence, specialize, assumption, crush.
some handy tacticals to try: ;, try, ||

Theorem forward_sim : forall c s c' s', step_com_fn c s = Some (c', s') -> step_com c s c' s'.
Admitted.

4. Prove that all steps in the relational semantics work in the functional semantics.

Theorem backward_sim : forall c s c' s', step_com c s c' s' -> step_com_fn c s = Some (c', s').
Admitted.

This page has been generated by coqdoc