Behavioral Equivalence

In the last chapter, we studied a simple transformation on arithmetic expressions. Our transformation was correct because it preserved the value of the expressions given as input. For Imp programs, correct transformations will be those that preserve the behavior of programs. In order to study those, we must first define the notion of program equivalence.

Definitions

For aexps and bexps with variables, the definition we want is clear. We say that two aexps or bexps are behaviorally equivalent if they evaluate to the same result in every state.

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 (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 both diverge or 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."

Examples

For examples of command equivalence, let's start by looking at some trivial program transformations involving SKIP:

Similarly, here is a simple transformations that simplifies IFB commands:

Of course, few programmers would be tempted to write a conditional whose guard is literally BTrue. A more interesting case is when the guard is equivalent to true: Theorem: If b is equivalent to BTrue, then IFB b THEN c1 ELSE c2 FI is equivalent to c1. Proof:

• (→) We must show, for all st and st', that if IFB b THEN c1 ELSE c2 FI / st ⇓ st' then c1 / st ⇓ st'.
  Proceed by cases on the rules that could possibly have been used to show IFB b THEN c1 ELSE c2 FI / st ⇓ st', namely E_IfTrue and E_IfFalse.
  • Suppose the final rule rule in the derivation of IFB b THEN c1 ELSE c2 FI / st ⇓ st' was E_IfTrue. We then have, by the premises of E_IfTrue, that c1 / st ⇓ st'. This is exactly what we set out to prove.
  • On the other hand, suppose the final rule in the derivation of IFB b THEN c1 ELSE c2 FI / st ⇓ st' was E_IfFalse. We then know that beval st b = false and c2 / st ⇓ st'.
    Recall that b is equivalent to BTrue, i.e. forall st, beval st b = beval st BTrue. In particular, this means that beval st b = true, since beval st BTrue = true. But this is a contradiction, since E_IfFalse requires that beval st b = false. Thus, the final rule could not have been E_IfFalse.
• (←) We must show, for all st and st', that if c1 / st ⇓ st' then IFB b THEN c1 ELSE c2 FI / st ⇓ st'.
  Since b is equivalent to BTrue, we know that beval st b = beval st BTrue = true. Together with the assumption that c1 / st ⇓ st', we can apply E_IfTrue to derive IFB b THEN c1 ELSE c2 FI / st ⇓ st'. ☐

Here is the formal version of this proof:

Similarly:

For WHILE loops, we can give a similar pair of theorems. A loop whose guard is equivalent to BFalse is equivalent to SKIP, while a loop whose guard is equivalent to BTrue is equivalent to WHILE BTrue DO SKIP END (or any other non-terminating program). The first of these facts is easy.

To prove the second fact, we need an auxiliary lemma stating that WHILE loops whose guards are equivalent to BTrue never terminate: Lemma: If b is equivalent to BTrue, then it cannot be the case that (WHILE b DO c END) / st ⇓ st'. Proof: Suppose that (WHILE b DO c END) / st ⇓ st'. We show, by induction on a derivation of (WHILE b DO c END) / st ⇓ st', that this assumption leads to a contradiction.

• Suppose (WHILE b DO c END) / st ⇓ st' is proved using rule E_WhileEnd. Then by assumption beval st b = false. But this contradicts the assumption that b is equivalent to BTrue.
• Suppose (WHILE b DO c END) / st ⇓ st' is proved using rule E_WhileLoop. Then we are given the induction hypothesis that (WHILE b DO c END) / st ⇓ st' is contradictory, which is exactly what we are trying to prove!
• Since these are the only rules that could have been used to prove (WHILE b DO c END) / st ⇓ st', the other cases of the induction are immediately contradictory. ☐

The Functional Equivalence Axiom

Finally, let's look at simple equivalences involving assignments. For example, we might expect to be able to show that X ::= AId X is equivalent to SKIP. However, when we try to show it, we get stuck in an interesting way.

Here we're stuck. The goal looks reasonable, but in fact it is not provable! If we look back at the set of lemmas we proved about update in the last chapter, we can see that lemma update_same almost does the job, but not quite: it says that the original and updated states agree at all values, but this is not the same thing as saying that they are = in Coq's sense! What's going on?

• States are function from ids to values
• Functions are equal when their definitions are syntactically the same (modulo simplification)
• Here we have two functions that behave the same on all inputs but are not syntactically the same.

This problem is actually quite general. If we try to prove other simple facts, such as or we'll get stuck in the same way: we'll have two functions that behave the same way on all inputs, but cannot be proven to be eq to each other. The reasoning principle we would like to use in these situations is called functional extensionality:

∀x, f x = g x
f = g

Although this principle is not derivable in Coq's built-in logic, it is safe to add it as an additional axiom.

With the benefit of this axiom we can prove our theorem.

Properties of Behavioral Equivalence

We now turn to developing some of the properties of the program equivalences we have defined.

Behavioral Equivalence is an Equivalence

First, we verify that the equivalences on aexps, bexps, and coms really are equivalences — i.e., that they are reflexive, symmetric, and transitive. The proofs are all easy.

Behavioral Equivalence is a Congruence

Less obviously, behavioral equivalence is also a congruence. That is, the equivalence of two subprograms implies the equivalence of the larger programs in which they are embedded:

aequiv a1 a1'
cequiv (i ::= a1) (i ::= a1')

cequiv c1 c1'
cequiv c2 c2'
cequiv (c1;;c2) (c1';;c2')

...and so on. (Note that we are using the inference rule notation here not as part of a definition, but simply to write down some valid implications in a readable format. We prove these implications below.) These properties allow us to reason that a large program behaves the same when we replace a small part with a new small part that behaves the same.

For example, here are two equivalent programs and a proof of their equivalence...

Case Study: Constant Folding

A program transformation is a function that takes a program as input and produces some variant of the program as its output. Compiler optimizations such as constant folding are a canonical example, but there are many others.

Soundness of Program Transformations

A program transformation is sound if it preserves the behavior of the original program. We can define a notion of soundness for translations of aexps, bexps, and coms.

The Constant-Folding Transformation

An expression is constant when it contains no variable references. Constant folding is an optimization that finds constant expressions and replaces them by their values.

Note that this version of constant folding doesn't eliminate trivial additions, etc. — we are focusing attention on a single optimization for the sake of simplicity. It is not hard to incorporate other ways of simplifying expressions; the definitions and proofs just get longer.

Not only can we lift fold_constants_aexp to bexps (in the BEq and BLe cases), we can also find constant boolean expressions and reduce them in-place.

To fold constants in a command, we apply the appropriate folding functions on all embedded expressions.

Soundness of Constant Folding

Now we need to show that what we've done is correct.

Proving That Programs Are Not Equivalent

Suppose that c1 is a command of the form X ::= a1;; Y ::= a2 and c2 is the command X ::= a1;; Y ::= a2', where a2' is formed by substituting a1 for all occurrences of X in a2. For example, c1 and c2 might be: Clearly, this particular c1 and c2 are equivalent. Is this true in general? Here, formally, is the function that substitutes an arithmetic expression for each occurrence of a given variable in another expression:

And here is the property we are interested in, expressing the claim that commands c1 and c2 as described above are always equivalent.

Sadly, the property does not always hold. Theorem: It is not the case that, for all i1, i2, a1, and a2, Proof: Suppose, for a contradiction, that for all i1, i2, a1, and a2, we have Consider the following program: Note that where st1 = { X ↦ 1, Y ↦ 1 }. By our assumption, we know that so, by the definition of cequiv, we have But we can also derive where st2 = { X ↦ 1, Y ↦ 2 }. Note that st1 ≠ st2; this is a contradiction, since ceval is deterministic! ☐