The small-step and large-step semantics are equivalent as captured by the following theorem.
Theorem. For all commands and stores and we have The proof is left as an exercise.
Non-Termination
For a given command and initial state , the execution of the command may terminate with some final store , or it may diverge and never yield a final state. For example, the command always diverges while diverges if and only if the value of variable in the initial state is positive.
If is a diverging configuration then there is no state such that However, in small-step semantics, diverging computations generate an infinite sequence: Hence, small-step semantics allow us to state and prove properties about programs that may diverge. Later in the notes, we will specify and prove properties that are of interest in potentially diverging computations.
Determinism
The semantics of IMP (both small-step and large-step) are deterministic. For example, each IMP command and each initial store evaluates to at most one final store.
Theorem. For all commands and stores , and , if and then .
To prove this theorem, we need an induction. But structural induction on the command will not work. (Why? Which case breaks?) Instead, we need to perform induction on the derivation of . We first introduce some useful notation.
Let be a derivation. We write if is a derivation of , that is, if the conclusion of is For example, if is the following derivation Then we have .
Let and be derivations. We say that is an immediate subderivation of if is a derivation of one of the premises used in the final rule in the derivation . For example, the derivation is an immediate subderivation of In a proof by induction on derivations, we assume that the property being proved holds for all immediate subderivations, and we show that it holds of the conclusion.
Proof. As , there is a derivation such that . Similarly, as , there is a derivation such that .
We proceed by induction on the derivation . We assume that the induction hypothesis holds for immediate subderivations of . In this case, the induction hypothesis is: We analyze the possible cases for the last rule used in .
Case SKIP: In this case and we have and . Since the rule is the only rule that has the command in its conclusion, the last rule used in 𝒟2 must also be , and so we have and the result holds.
Case ASSGN: In this case and we have and . The last rule used in must also be , and so we have and the result holds. Strictly speaking, we also need to argue that the evaluation of is deterministic. In this proof we will tacitly assume deterministic evaluation of arithmetic and boolean expressions.
Case SEQ: In this case and we have . The last rule used in must also be , and so we have By the inductive hypothesis applied to the derivation , we have . By another application of the inductive hypothesis to , we have and the result holds.
Case IF-T: Here we have and we have . The last rule used in must also be IF-T and so we have The result holds by the inductive hypothesis applied to the derivation .
Case IF-F: Similar to the case for IF-T.
Case WHILE-F: Straightforward, similar to the case for SKIP.
Case WHILE-T: Here we have and we have . The last rule used in must also be WHILE-T, and so we have By the inductive hypothesis applied to the derivation , we have . By another application of the inductive hypothesis to the derivation , we have and the result holds.
Note that even though appears in the derivation of , we do not run in to problems, as the induction is over the derivation, not over the structure of the command.
