EquivProgram Equivalence

Behavioral Equivalence

In the last chapter, we studied a simple transformation 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.

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)%imp 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').
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

For examples of command equivalence, let's start by looking at some trivial program transformations involving SKIP:
Theorem skip_left : ∀c,
  cequiv
    (SKIP;; c)
    c.
Proof.
  (* WORK IN CLASS *) Admitted.

Similarly, here is a simple transformation that optimizes TEST commands:
Theorem TEST_true_simple : ∀c1 c2,
  cequiv
    (TEST true THEN c1 ELSE c2 FI)
    c1.

Of course, no (human) programmer would write a conditional whose guard is literally true. But they might write one whose guard is equivalent to true:
Theorem TEST_true: ∀b c1 c2,
  bequiv b BTrue →
  cequiv
    (TEST b THEN c1 ELSE c2 FI)
    c1.
Similarly:
Theorem TEST_false : ∀b c1 c2,
  bequiv b BFalse →
  cequiv
    (TEST b THEN c1 ELSE c2 FI)
    c2.

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.
Theorem WHILE_false : ∀b c,
  bequiv b BFalse →
  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 BTrue never terminate.
Lemma WHILE_true_nonterm : ∀b c st st',
  bequiv b BTrue →
  ~( 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 a common transformation in real compilers.
Theorem loop_unrolling : ∀b c,
  cequiv
    (WHILE b DO c END)
    (TEST b THEN (c ;; WHILE b DO c END) ELSE SKIP FI).
Proof.
  (* WORK IN CLASS *) Admitted.

Properties of Behavioral Equivalence

We next consider some fundamental properties of program equivalence.

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.
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 iff_trans : ∀(P1 P2 P3 : Prop),
  (P1 ↔ P2) → (P2 ↔ P3) → (P1 ↔ P3).
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 a1 a1'  
cequiv (x ::= a1) (x ::= a1')
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 CAss_congruence : ∀x a1 a1',
  aequiv a1 a1' →
  cequiv (CAss x a1) (CAss x a1').
Theorem CWhile_congruence : ∀b1 b1' c1 c1',
  bequiv b1 b1' → cequiv c1 c1' →
  cequiv (WHILE b1 DO c1 END) (WHILE b1' DO c1' 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 (TEST b THEN c1 ELSE c2 FI)
         (TEST b' THEN c1' ELSE c2' FI).

For example, here are two equivalent programs and a proof of their equivalence...
Example congruence_example:
  cequiv
    (* Program 1: *)
    (X ::= 0;;
     TEST X = 0
     THEN
       Y ::= 0
     ELSE
       Y ::= 42
     FI)
    (* Program 2: *)
    (X ::= 0;;
     TEST X = 0
     THEN
       Y ::= X - X (* <--- Changed here *)
     ELSE
       Y ::= 42
     FI).
Proof.
  apply CSeq_congruence.
  - apply refl_cequiv.
  - apply CIf_congruence.
    + apply refl_bequiv.
    + apply CAss_congruence. unfold aequiv. simpl.
      * symmetry. apply minus_diag.
    + apply refl_cequiv.
Qed.

Program Transformations

A program transformation is a function that takes a program as input and produces some variant of the program as output. Compiler optimizations such as constant folding are a canonical example, but there are many others.
A program transformation is 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 when 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
  | APlus a1 a2 ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (n1 + n2)
    | (a1', a2') ⇒ APlus a1' a2'
    end
  | AMinus a1 a2 ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (n1 - n2)
    | (a1', a2') ⇒ AMinus a1' a2'
    end
  | AMult a1 a2 ⇒
    match (fold_constants_aexp a1,
           fold_constants_aexp a2)
    with
    | (ANum n1, ANum n2) ⇒ ANum (n1 * n2)
    | (a1', a2') ⇒ AMult a1' a2'
    end
  end.
(* *** *)
Example fold_aexp_ex1 :
    fold_constants_aexp ((1 + 2) * X)
  = (3 * X)%imp.
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.
Example fold_aexp_ex2 :
  fold_constants_aexp (X - ((0 * 6) + Y))%imp = (X - (0 + Y))%imp.

Not only can we lift fold_constants_aexp to bexps (in the BEq and BLe cases); we can also look for constant boolean expressions and evaluate them in-place.
Fixpoint fold_constants_bexp (b : bexp) : bexp :=
  match b with
  | BTrue ⇒ BTrue
  | BFalse ⇒ BFalse
  | BEq a1 a2 ⇒
      match (fold_constants_aexp a1,
             fold_constants_aexp a2) with
      | (ANum n1, ANum n2) ⇒
          if n1 =? n2 then BTrue else BFalse
      | (a1', a2') ⇒
          BEq a1' a2'
      end
  | BLe a1 a2 ⇒
      match (fold_constants_aexp a1,
             fold_constants_aexp a2) with
      | (ANum n1, ANum n2) ⇒
          if n1 <=? n2 then BTrue else BFalse
      | (a1', a2') ⇒
          BLe a1' a2'
      end
  | BNot b1 ⇒
      match (fold_constants_bexp b1) with
      | BTrue ⇒ BFalse
      | BFalse ⇒ BTrue
      | b1' ⇒ BNot b1'
      end
  | BAnd b1 b2 ⇒
      match (fold_constants_bexp b1,
             fold_constants_bexp b2) with
      | (BTrue, BTrue) ⇒ BTrue
      | (BTrue, BFalse) ⇒ BFalse
      | (BFalse, BTrue) ⇒ BFalse
      | (BFalse, BFalse) ⇒ BFalse
      | (b1', b2') ⇒ BAnd b1' b2'
      end
  end.
(* *** *)
Example fold_bexp_ex1 :
  fold_constants_bexp (true && ~(false && true))%imp
  = true.
Example fold_bexp_ex2 :
  fold_constants_bexp ((X = Y) && (0 = (2 - (1 + 1))))%imp
  = ((X = Y) && true)%imp.

To fold constants in a command, we apply the appropriate folding functions on all embedded expressions.
Open Scope imp.
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)
  | TEST b THEN c1 ELSE c2 FI ⇒
      match fold_constants_bexp b with
      | BTrue ⇒ fold_constants_com c1
      | BFalse ⇒ fold_constants_com c2
      | b' ⇒ TEST b' THEN fold_constants_com c1
                     ELSE fold_constants_com c2 FI
      end
  | WHILE b DO c END ⇒
      match fold_constants_bexp b with
      | BTrue ⇒ WHILE BTrue DO SKIP END
      | BFalse ⇒ SKIP
      | b' ⇒ WHILE b' DO (fold_constants_com c) END
      end
  end.
Close Scope imp.

Example fold_com_ex1 :
  fold_constants_com
    (* Original program: *)
    (X ::= 4 + 5;;
     Y ::= X - 3;;
     TEST (X - Y) = (2 + 4) THEN SKIP
     ELSE Y ::= 0 FI;;
     TEST 0 ≤ (4 - (2 + 1)) THEN Y ::= 0
     ELSE SKIP FI;;
     WHILE Y = 0 DO
       X ::= X + 1
     END)%imp
  = (* After constant folding: *)
    (X ::= 9;;
     Y ::= X - 3;;
     TEST (X - Y) = 6 THEN SKIP
     ELSE Y ::= 0 FI;;
     Y ::= 0;;
     WHILE Y = 0 DO
       X ::= X + 1
     END)%imp.

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

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 eqb_string x x' then u else AId x'
  | APlus a1 a2 ⇒
      APlus (subst_aexp x u a1) (subst_aexp x u a2)
  | AMinus a1 a2 ⇒
      AMinus (subst_aexp x u a1) (subst_aexp x u a2)
  | AMult a1 a2 ⇒
      AMult (subst_aexp x u a1) (subst_aexp x u a2)
  end.
Example subst_aexp_ex :
  subst_aexp X (42 + 53) (Y + X)%imp
  = (Y + (42 + 53))%imp.

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 := ∀x1 x2 a1 a2,
  cequiv (x1 ::= a1;; x2 ::= a2)
         (x1 ::= a1;; x2 ::= subst_aexp x1 a1 a2).

Sadly, the property does not always hold — i.e., it is not the case that, for all x1, x2, a1, and a2,
      cequiv (x1 ::= a1;; x2 ::= a2)
             (x1 ::= a1;; x2 ::= subst_aexp x1 a1 a2).
To see this, suppose (for a contradiction) that for all x1, x2, a1, and a2, we have
      cequiv (x1 ::= a1;; x2 ::= a2)
             (x1 ::= a1;; x2 ::= subst_aexp x1 a1 a2).
Consider the following program:
      X ::= X + 1;; Y ::= X
Note that
      empty_st =[ X ::= X + 1;; Y ::= X ]⇒ st1,
where st1 = (Y !-> 1 ; X !-> 1).
By assumption, we know that
      cequiv (X ::= X + 1;;
              Y ::= X)
             (X ::= X + 1;;
              Y ::= X + 1)
so, by the definition of cequiv, we have
      empty_st =[ X ::= X + 1;; Y ::= X + 1 ]⇒ st1.
But we can also derive
      empty_st =[ X ::= X + 1;; Y ::= X + 1 ]⇒ st2,
where st2 = (Y !-> 2 ; X !-> 1). But st1 ≠ st2, which is a contradiction, since ceval is deterministic! ☐
Theorem subst_inequiv :
  ¬subst_equiv_property.