4.1.1. Definitions🔗

For Aexps and Bexps with variables, the definition we want is clear: two Aexps or Bexps are "behaviorally equivalent" if they evaluate to the same result in every state.

We'll also define a type class Equiv, so that these relations (and the one for commands, below) can all be written with the notation ≃.

Here are some simple examples of equivalences of arithmetic and boolean expressions.

For commands, the situation is a little more subtle. We can't simply say "two commands are behaviorally equivalent if they evaluate to the same ending state whenever they are started in the same initial state," because some commands, when run in some starting states, don't terminate in any final state at all!

What we need instead is this: two commands are behaviorally equivalent if, for any given starting state, they either (1) both diverge or else (2) both terminate in the same final state. A compact way to express this is "if the first one terminates in a particular state then so does the second, and vice versa."

X := 1;
Y := 2

Y := 2;
X := 1

X := 1;
Y := 2

X := 2;
Y := 1

while (1 ≤ X) {
  X := X + 1
}

while (2 ≤ X) {
  X := X + 1
}

while (true) {
  while (false) { X := X + 1 }
}

while (false) {
  while (true) { X := X + 1 }
}

4.1.2. Simple Examples🔗

For examples of command equivalence, let's start by looking at a trivial equivalence involving skip.

Similarly, here is a simple equivalence that optimizes if commands.

Of course, no programmer would write a conditional whose condition is literally true. (At least, no human programmer - compilers and macro preprocessors do this sort of thing internally all the time!) But they might write one whose condition is equivalent to true:

Theorem: If b is equivalent to true, then if (b) {c₁} else {c₂} is equivalent to c₁. Proof:

• (→) We must show, for all st and st', that if st =[ imp {if (b) {c₁} else {c₂}} ]=> st' then st =[ c₁ ]=> st'.

  Proceed by cases on the rules that could possibly have been used to show st =[ imp {if (b) {c₁} else {c₂}} ]=> st', namely Com.EvalR.ifTrue and Com.EvalR.ifFalse.

  • Suppose the final rule in the derivation of st =[ imp {if (b) {c₁} else {c₂}} ]=> st' was Com.EvalR.ifTrue. We then have, by the premises of Com.EvalR.ifTrue, that st =[ c₁ ]=> st'. This is exactly what we set out to prove.

  • On the other hand, suppose the final rule in the derivation of st =[ imp {if (b) {c₁} else {c₂}} ]=> st' was Com.EvalR.ifFalse. We then know that b.eval st = false and st =[ c₂ ]=> st'.

    Recall that b is equivalent to true, i.e., for all st, b.eval st = (bexp {true}).eval st. In particular, this means that b.eval st = true, since (bexp {true}).eval st = true. But this is a contradiction, since Com.EvalR.ifFalse requires that b.eval st = false. Thus, the final rule could not have been Com.EvalR.ifFalse.

• (←) We must show, for all st and st', that if st =[ c₁ ]=> st' then st =[ imp {if (b) {c₁} else {c₂}} ]=> st'.

  Since b is equivalent to true, we know that b.eval st = (bexp {true}).eval st = true. Together with the assumption that st =[ c₁ ]=> st', we can apply Com.EvalR.ifTrue to derive st =[ imp {if (b) {c₁} else {c₂}} ]=> st'.

Here is the formal version of this proof: