EquivProgram Equivalence

Behavioral Equivalence

In the Imp, we defined a simple optimization on arithmetic expressions and showed that it was correct in the sense that it preserved the value of the expressions.
To play a similar game with programs involving mutable state, we need a more sophisticated notion of correctness, called behavioral equivalence.
For example:
  • X + 2 is behaviorally equivalent to 1 + X + 1
  • X - X is behaviorally equivalent to 0
  • (X - 1) + 1 is not behaviorally equivalent to X

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.
Definition aequiv (a1 a2 : aexp) : Prop :=
  ∀ (st : state),
    aeval st a1 = aeval st a2.
Definition bequiv (b1 b2 : bexp) : Prop :=
  ∀ (st : state),
    beval st b1 = beval st b2.
Theorem aequiv_example:
  aequiv
    <{ X - X }>
    <{ 0 }>.
Theorem bequiv_example:
  bequiv
    <{ X - X = 0 }>
    <{ true }>.

For commands, we need to deal with the possibility of nontermination.
We do this by defining command equivalence as "if the first one terminates in a particular state then so does the second, and vice versa":
Definition cequiv (c1 c2 : com) : Prop :=
  ∀ (st st' : state),
    (st =[ c1 ]=> st') ↔ (st =[ c2 ]=> st').

We can also define an asymmetric variant of this relation: We say that c1 refines c2 if they produce the same final states when c1 terminates (but c1 may not terminate in some cases where c2 does).
Definition refines (c1 c2 : com) : Prop :=
  ∀ (st st' : state),
    (st =[ c1 ]=> st') → (st =[ c2 ]=> st').
Are these two programs equivalent?
    X := 1;
    Y := 2 and
    Y := 2;
    X := 1
(1) Yes
(2) No
(3) Not sure
What about these?
    X := 1;
    Y := 2 and
    X := 2;
    Y := 1
(1) Yes
(2) No
(3) Not sure
What about these?
    while 1 ≤ X do
      X := X + 1
    end and
    while 2 ≤ X do
      X := X + 1
    end
(1) Yes
(2) No
(3) Not sure
These?
    while true do
      while false do X := X + 1 end
    end and
    while false do
      while true do X := X + 1 end
    end
(1) Yes
(2) No
(3) Not sure

Simple Examples

Theorem skip_left : ∀ c,
  cequiv
    <{ skip; c }>
    c.
Proof.
  (* WORK IN CLASS *) Admitted.

Similarly, here is a simple equivalence that optimizes if commands:
Theorem if_true_simple : ∀ c1 c2,
  cequiv
    <{ if true then c1 else c2 end }>
    c1.

Of course, no (human) programmer would write a conditional whose condition is literally true. But they might write one whose condition is equivalent to true:
Theorem if_true: ∀ b c1 c2,
  bequiv b <{true}> →
  cequiv
    <{ if b then c1 else c2 end }>
    c1.

Similarly:
Theorem if_false : ∀ b c1 c2,
  bequiv b <{false}> →
  cequiv
    <{ if b then c1 else c2 end }>
    c2.

For while loops, we can give a similar pair of theorems. A loop whose guard is equivalent to false is equivalent to skip, while a loop whose guard is equivalent to true is equivalent to while true do skip end (or any other non-terminating program).

The first of these facts is easy.
Theorem while_false : ∀ b c,
  bequiv b <{false}> →
  cequiv
    <{ while b do c end }>
    <{ skip }>.

To prove the second fact, we need an auxiliary lemma stating that while loops whose guards are equivalent to true never terminate.
Lemma while_true_nonterm : ∀ b c st st',
  bequiv b <{true}> →
  ~( st =[ while b do c end ]=> st' ).
Proof.
  (* WORK IN CLASS *) Admitted.
Theorem while_true : ∀ b c,
  bequiv b <{true}> →
  cequiv
    <{ while b do c end }>
    <{ while true do skip end }>.

A more interesting fact about while commands is that any number of copies of the body can be "unrolled" without changing meaning.
Loop unrolling is an important transformation in any real compiler: its correctness is of more than academic interest!
Theorem loop_unrolling : ∀ b c,
  cequiv
    <{ while b do c end }>
    <{ if b then c ; while b do c end else skip end }>.
Proof.
  (* WORK IN CLASS *) Admitted.

Properties of Behavioral Equivalence

We next consider some fundamental properties of program equivalence.

Behavioral Equivalence Is an Equivalence

First, let's 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.
Lemma refl_aequiv : ∀ (a : aexp),
  aequiv a a.
Lemma sym_aequiv : ∀ (a1 a2 : aexp),
  aequiv a1 a2 → aequiv a2 a1.
Lemma trans_aequiv : ∀ (a1 a2 a3 : aexp),
  aequiv a1 a2 → aequiv a2 a3 → aequiv a1 a3.
Lemma refl_bequiv : ∀ (b : bexp),
  bequiv b b.
Lemma sym_bequiv : ∀ (b1 b2 : bexp),
  bequiv b1 b2 → bequiv b2 b1.
Lemma trans_bequiv : ∀ (b1 b2 b3 : bexp),
  bequiv b1 b2 → bequiv b2 b3 → bequiv b1 b3.
Lemma refl_cequiv : ∀ (c : com),
  cequiv c c.
Lemma sym_cequiv : ∀ (c1 c2 : com),
  cequiv c1 c2 → cequiv c2 c1.
Lemma trans_cequiv : ∀ (c1 c2 c3 : com),
  cequiv c1 c2 → cequiv c2 c3 → cequiv c1 c3.

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 a a'  
cequiv (x := a) (x := a')
cequiv c1 c1'
cequiv c2 c2'  
cequiv (c1;c2) (c1';c2')
... and so on for the other forms of commands.

These properties allow us to reason that a large program behaves the same when we replace a small part with something equivalent.
Theorem CAsgn_congruence : ∀ x a a',
  aequiv a a' →
  cequiv <{x := a}> <{x := a'}>.

Theorem CWhile_congruence : ∀ b b' c c',
  bequiv b b' → cequiv c c' →
  cequiv <{ while b do c end }> <{ while b' do c' end }>.
Proof.
  (* WORK IN CLASS *) Admitted.

Theorem CSeq_congruence : ∀ c1 c1' c2 c2',
  cequiv c1 c1' → cequiv c2 c2' →
  cequiv <{ c1;c2 }> <{ c1';c2' }>.

Theorem CIf_congruence : ∀ b b' c1 c1' c2 c2',
  bequiv b b' → cequiv c1 c1' → cequiv c2 c2' →
  cequiv <{ if b then c1 else c2 end }>
         <{ if b' then c1' else c2' end }>.

For example, here are two equivalent programs and a proof of their equivalence using these congruence theorems...
Example congruence_example:
  cequiv
    (* Program 1: *)
    <{ X := 0;
       if X = 0 then Y := 0
       else Y := 42 end }>
    (* Program 2: *)
    <{ X := 0;
       if X = 0 then Y := X - X (* <--- Changed here *)
       else Y := 42 end }>.
Proof.
  apply CSeq_congruence.
  - apply refl_cequiv.
  - apply CIf_congruence.
    + apply refl_bequiv.
    + apply CAsgn_congruence. unfold aequiv. simpl.
      symmetry. apply sub_diag.
    + apply refl_cequiv.
Qed.

Program Transformations

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

A program transformation is said to be sound if it preserves the behavior of the original program.
Definition atrans_sound (atrans : aexp → aexp) : Prop :=
  ∀ (a : aexp),
    aequiv a (atrans a).
Definition btrans_sound (btrans : bexp → bexp) : Prop :=
  ∀ (b : bexp),
    bequiv b (btrans b).
Definition ctrans_sound (ctrans : com → com) : Prop :=
  ∀ (c : com),
    cequiv c (ctrans c).

The Constant-Folding Transformation

An expression is constant if it contains no variable references.
Constant folding is an optimization that finds constant expressions and replaces them by their values.
Fixpoint fold_constants_aexp (a : aexp) : aexp :=
  match a with
  | ANum n ⇒ ANum n
  | AId x ⇒ AId x
  | <{ a1 + a2 }> ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (n1 + n2)
    | (a1', a2') ⇒ <{ a1' + a2' }>
    end
  | <{ a1 - a2 }> ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (n1 - n2)
    | (a1', a2') ⇒ <{ a1' - a2' }>
    end
  | <{ a1 × a2 }> ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (n1 × n2)
    | (a1', a2') ⇒ <{ a1' × a2' }>
    end
  end.

Example fold_aexp_ex1 :
    fold_constants_aexp <{ (1 + 2) × X }>
  = <{ 3 × X }>.
Example fold_aexp_ex2 :
  fold_constants_aexp <{ X - ((0 × 6) + Y) }> = <{ X - (0 + Y) }>.

Not only can we lift fold_constants_aexp to bexps (in the BEq, BNeq, and BLe cases); we can also look for constant boolean expressions and evaluate them in-place as well.
Fixpoint fold_constants_bexp (b : bexp) : bexp :=
  match b with
  | <{true}> ⇒ <{true}>
  | <{false}> ⇒ <{false}>
  | <{ a1 = a2 }> ⇒
      match (fold_constants_aexp a1,
             fold_constants_aexp a2) with
      | (ANum n1, ANum n2) ⇒
          if n1 =? n2 then <{true}> else <{false}>
      | (a1', a2') ⇒
          <{ a1' = a2' }>
      end
  | <{ a1 ≠ a2 }> ⇒
      match (fold_constants_aexp a1,
             fold_constants_aexp a2) with
      | (ANum n1, ANum n2) ⇒
          if negb (n1 =? n2) then <{true}> else <{false}>
      | (a1', a2') ⇒
          <{ a1' ≠ a2' }>
      end
  | <{ a1 ≤ a2 }> ⇒
      match (fold_constants_aexp a1,
             fold_constants_aexp a2) with
      | (ANum n1, ANum n2) ⇒
          if n1 <=? n2 then <{true}> else <{false}>
      | (a1', a2') ⇒
          <{ a1' ≤ a2' }>
      end
  | <{ a1 > a2 }> ⇒
      match (fold_constants_aexp a1,
             fold_constants_aexp a2) with
      | (ANum n1, ANum n2) ⇒
          if n1 <=? n2 then <{false}> else <{true}>
      | (a1', a2') ⇒
          <{ a1' > a2' }>
      end
  | <{ ¬b1 }> ⇒
      match (fold_constants_bexp b1) with
      | <{true}> ⇒ <{false}>
      | <{false}> ⇒ <{true}>
      | b1' ⇒ <{ ¬b1' }>
      end
  | <{ b1 && b2 }> ⇒
      match (fold_constants_bexp b1,
             fold_constants_bexp b2) with
      | (<{true}>, <{true}>) ⇒ <{true}>
      | (<{true}>, <{false}>) ⇒ <{false}>
      | (<{false}>, <{true}>) ⇒ <{false}>
      | (<{false}>, <{false}>) ⇒ <{false}>
      | (b1', b2') ⇒ <{ b1' && b2' }>
      end
  end.

Example fold_bexp_ex1 :
  fold_constants_bexp <{ true && ~(false && true) }>
  = <{ true }>.
Example fold_bexp_ex2 :
  fold_constants_bexp <{ (X = Y) && (0 = (2 - (1 + 1))) }>
  = <{ (X = Y) && true }>.

To fold constants in a command, we apply the appropriate folding functions on all embedded expressions.
Fixpoint fold_constants_com (c : com) : com :=
  match c with
  | <{ skip }> ⇒
      <{ skip }>
  | <{ x := a }> ⇒
      <{ x := (fold_constants_aexp a) }>
  | <{ c1 ; c2 }> ⇒
      <{ fold_constants_com c1 ; fold_constants_com c2 }>
  | <{ if b then c1 else c2 end }> ⇒
      match fold_constants_bexp b with
      | <{true}> ⇒ fold_constants_com c1
      | <{false}> ⇒ fold_constants_com c2
      | b' ⇒ <{ if b' then fold_constants_com c1
                       else fold_constants_com c2 end}>
      end
  | <{ while b do c1 end }> ⇒
      match fold_constants_bexp b with
      | <{true}> ⇒ <{ while true do skip end }>
      | <{false}> ⇒ <{ skip }>
      | b' ⇒ <{ while b' do (fold_constants_com c1) end }>
      end
  end.

Example fold_com_ex1 :
  fold_constants_com
    (* Original program: *)
    <{ X := 4 + 5;
       Y := X - 3;
       if (X - Y) = (2 + 4) then skip
       else Y := 0 end;
       if 0 ≤ (4 - (2 + 1)) then Y := 0
       else skip end;
       while Y = 0 do
         X := X + 1
       end }>
  = (* After constant folding: *)
    <{ X := 9;
       Y := X - 3;
       if (X - Y) = 6 then skip
       else Y := 0 end;
       Y := 0;
       while Y = 0 do
         X := X + 1
       end }>.

Soundness of Constant Folding

Now we need to show that what we've done is correct.
Theorem fold_constants_aexp_sound :
  atrans_sound fold_constants_aexp.
Theorem fold_constants_bexp_sound:
  btrans_sound fold_constants_bexp.
Theorem fold_constants_com_sound :
  ctrans_sound fold_constants_com.

Proving Inequivalence

Next, let's look at some programs that 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:
       c1 = (X := 42 + 53;
               Y := Y + X)
       c2 = (X := 42 + 53;
               Y := Y + (42 + 53)) Clearly, this particular c1 and c2 are equivalent. Is this true in general?

More formally, here is the function that substitutes an arithmetic expression u for each occurrence of a given variable x in another expression a:
Fixpoint subst_aexp (x : string) (u : aexp) (a : aexp) : aexp :=
  match a with
  | ANum n ⇒
      ANum n
  | AId x' ⇒
      if String.eqb x x' then u else AId x'
  | <{ a1 + a2 }> ⇒
      <{ (subst_aexp x u a1) + (subst_aexp x u a2) }>
  | <{ a1 - a2 }> ⇒
      <{ (subst_aexp x u a1) - (subst_aexp x u a2) }>
  | <{ a1 × a2 }> ⇒
      <{ (subst_aexp x u a1) × (subst_aexp x u a2) }>
  end.
Example subst_aexp_ex :
  subst_aexp X <{42 + 53}> <{Y + X}>
  = <{ Y + (42 + 53)}>.

And here is the property we are interested in, expressing the claim that commands c1 and c2 as described above are always equivalent.
Definition subst_equiv_property : Prop := ∀ x1 x2 a1 a2,
  cequiv <{ x1 := a1; x2 := a2 }>
         <{ x1 := a1; x2 := subst_aexp x1 a1 a2 }>.

Sadly, the property does not always hold.
Here is a counterexample:
       X := X + 1; Y := X If we perform the substitution, we get
       X := X + 1; Y := X + 1 which clearly isn't equivalent.
Theorem subst_inequiv :
  ¬subst_equiv_property.