# 「软件基础 - PLF」 1. Program Equivalence 程序的等价关系

Posted by Hux on March 1, 2019

### issues on coqc module linking

Some module (e.g.Map) not found either maunally make map.vo or proof general can solve that.

## Behavioral Equivalence 行为等价

How to define the correctness of program transformation, e.g. optimize_0plus ?

• in the setting w/o var (imp w/o var and state) : yield a program the evals to same number as original.
• in the setting w/ var (full imp w/ assignment) : we need to consider the role of var and state.

### Definitions

Two aexps or bexps are behaviorally equivalent if they evaluate to the same result in every state.

1
2
3
4
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.


For commands, We can’t simply say … if they evaluate to the same ending state some commands don’t terminate in any final state at all!

So to define, they either or…

1. both diverge 都发散
2. both terminate in the same final state 都在同一个状态停机

A compact way is

“if the first one terminates in a particular state then so does the second, and vice versa.”

1
2
3
Definition cequiv (c1 c2 : com) : Prop :=
∀(st st' : state),
(st =[ c1 ]⇒ st') ↔ (st =[ c2 ]⇒ st').


### Example 1 - Simple (but demonstrated)

1
2
3
4
5
6
7
8
9
10
11
12
13
Theorem skip_left : forall c,
cequiv (SKIP;; c) c.
Proof.
intros c st st'. split; intros H.
- (* -> *)
inversion H; subst.  (* inverse E_Seq   *)
inversion H2. subst. (* inverse E_Skip  *)
assumption.
- (* <- *)             (* reversely *)
apply E_Seq with st. (* apply E_Seq *)
apply E_Skip.        (* apply E_Skip *)
assumption.
Qed.


Noticed that the inversion is like use the inverse function of constructors.

### Example 2 - WHILE true non-terminating

one interesting theorem is that we can prove WHILE <things ⇓ true> is not terminating. and is equivalent to any other non-terminating program, e.g. WHILE BTrue DO SKIP END: (因为我们的「等价」只要求同「发散」即可)

1
2
3
4
5
Theorem WHILE_true : ∀b c,
bequiv b true →
cequiv
(WHILE b DO c END)
(WHILE true DO SKIP END).


### Example 3 - Loop Unrolling

any number of copies of the body can be “unrolled” without changing meaning

1
2
3
4
Theorem loop_unrolling : ∀b c,
cequiv
(WHILE b DO c END)
(TEST b THEN (c ;; WHILE b DO c END) ELSE SKIP FI).    (** 展开一层 **)


### Example 4 - Use of extenionality 外延性

x !-> m x ; x is same map with m by extenionality!

1
2
Theorem identity_assignment : ∀x,
cequiv (x ::= x) SKIP.


## Properties of Behavioral Equivalence 行为等价的性质

### 同余关系（Congruence）

That is, the equivalence of two subprograms implies the equivalence of the larger programs in which they are embedded 如果两个子程序等价，那么当二者所在的更大的程序中_只有二者不同_时， 这两个更大的程序也等价

1
2
3
4
5
6
7
8
aequiv a1 a1'
-----------------------------
cequiv (x ::= a1) (x ::= a1')

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


1
2
3
4
Theorem CAss_congruence : ∀x a1 a1',     (** cequiv 是集合 commands 上的等价关系 **)
aequiv a1 a1' →
cequiv (CAss x a1) (CAss x a1').       (** 在 CAss 这个 operation 下保持等价 => 同余 **)
cequiv (x ::= a1) (x ::= a1').         (** 或，在 ::= 这个 command 下保持等价 => 同余 **)


I guess…“both terminating” relation? which is equivalence relation on commands, but the equivalence would not be maintained after, say C_WHILE operation.

### Example - Using Congruence

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
Example congruence_example:
cequiv
(* 程序 1： *)
(X ::= 0;;
TEST X = 0
THEN
Y ::= 0
ELSE
Y ::= 42
FI)
(* 程序 2： *)
(X ::= 0;;
TEST X = 0
THEN
Y ::= X - X (* <--- 这里不同 *)
ELSE
Y ::= 42
FI).
Proof.
apply CSeq_congruence.
- apply refl_cequiv.
- apply CIf_congruence.
+ apply refl_bequiv.
+ apply CAss_congruence.     (** <--- 化简到只需要证明 aequiv 0 (X - X) **)
unfold aequiv. simpl.
* symmetry. apply minus_diag.
+ apply refl_cequiv.
Qed.


## Program Transformations 程序变换

A program transformation is sound if it preserves the behavior of the original program. 如果一个程序变换保留了其原始行为，那么它就是_可靠_的

• 当我们的 datatype 是 constructor 时 => 不交并
• 当我们的 datatype 有 recursive 时 => 集合的递归定义
1
2
3
4
5
6
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).


### Constant Folding 常量折叠

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. 常量折叠是一种找到常量表达式并把它们替换为其值的优化方法。

### Soundness of Constant Folding

#### aexp

1
2
3
4
5
6
7
8
9
10
11
12
Theorem fold_constants_aexp_sound :
atrans_sound fold_constants_aexp.
Proof.
unfold atrans_sound. intros a. unfold aequiv. intros st.

(** 这个时候的状态：**)

a : aexp
st : state
============================
aeval st a = aeval st (fold_constants_aexp a)



#### bexp

1
2
3
4
5
6
7
8
9
10
11
12
(** 如果不记住而是直接 destruct 的话，这部分信息就丢失了 **)
remember (fold_constants_aexp a1) as a1' eqn:Heqa1'.
remember (fold_constants_aexp a2) as a2' eqn:Heqa2'.

(** 保留了这部分信息的目的是，使用 aexp 的可靠性定理来建立 aexp 与 值 的关系 **)
replace (aeval st a1) with (aeval st a1') by
(subst a1'; rewrite <- fold_constants_aexp_sound; reflexivity).
replace (aeval st a2) with (aeval st a2') by
(subst a2'; rewrite <- fold_constants_aexp_sound; reflexivity).

(** 最后才分类讨论 **)
destruct a1'; destruct a2'; try reflexivity.


### Soundness of (0 + n)

1
2
3
4
Theorem trans_ctrans_sound : forall tr1 tr2,
ctrans_sound tr1 ->
ctrans_sound tr2 ->
ctrans_sound (fun c => tr2 (tr1 c)).


## Proving Inequivalence 证明程序不等价

1
2
3
4
(**    [X := 42 + 53](Y + X)  =>  Y + (42 + 53)    **)
Example subst_aexp_ex :
subst_aexp X (42 + 53) (Y + X)%imp = (Y + (42 + 53))%imp.
Proof. reflexivity. Qed.


1
2
3
Definition subst_equiv_property := ∀x1 x2 a1 a2,
cequiv (x1 ::= a1;; x2 ::= a2)
(x1 ::= a1;; x2 ::= subst_aexp x1 a1 a2).


Informal proof

• provide a witness

Formal

• give counterexamples via remember, then show ⊥.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
(** 给出一组反例，使用性质证明他们 cequiv **)

remember (X ::= X + 1;;
Y ::= X)%imp     as c1.
remember (X ::= X + 1;;
Y ::= X + 1)%imp as c2.
assert (cequiv c1 c2) by (subst; apply Contra).

(* => *)  Heqc1 : c1 = (X ::= X + 1;; Y ::= X)%imp
Heqc2 : c2 = (X ::= X + 1;; Y ::= X + 1)%imp
H : cequiv c1 c2
============================
False

(** 给出他们将 eval 出不同的 heap **)

remember (Y !-> 1 ; X !-> 1) as st1.
remember (Y !-> 2 ; X !-> 1) as st2.
assert (H1 : empty_st =[ c1 ]=> st1);
assert (H2 : empty_st =[ c2 ]=> st2);

apply H in H1. (** 使用 H : cequiv c1 c2 , 我们得到 **)

(* => *)  H1 : empty_st =[ c2 ]=> st1
H2 : empty_st =[ c2 ]=> st2
============================
False

(** 利用 ceval 的 deterministic **)

assert (Hcontra : st1 = st2)
by (apply (ceval_deterministic c2 empty_st); assumption).

(* => *)  Hcontra : st1 = st2
============================
False

(** st1, st2 are map, which are actually function!
这时我们可以反用 functional extenionality，直接 apply Y 然后 discrinminate **)

assert (Hcontra' : st1 Y = st2 Y)
by (rewrite Hcontra; reflexivity).
subst. inversion Hcontra'.  Qed.


## Extended Exercise: Nondeterministic Imp

HAVOC roughly corresponds to an uninitialized variable in a low-level language like C. After the HAVOC, the variable holds a fixed but arbitrary number.

1
2
3
4
5
6
7
8
9
10
11
12
Inductive com : Type :=
...
| CHavoc : string → com. (* <--- 新增 *)

Notation "'HAVOC' l" :=
(CHavoc l) (at level 60) : imp_scope.

Inductive ceval : com -> state -> state -> Prop :=
...
| E_Havoc : forall st (n : nat) x,
st =[ HAVOC x ]=> (x !-> n)        (** can eval to arbitraty heap **)


# Small-Step

## deterministic

also the def of partial function?

solve_by_inverts

in LTac. (used to generate proof) LTac doesn’t have termination check. (might not be able to find…)

match is back-tracking point.

number passing in = depth of the iteration/recursion

ST_Plus2 need value v1. not redundant with ST_Plus1 we might have things not value but cannot take step as well.

Strong Progress

Normal form

= no relation related to (so cannot step to)

vs Value…

destruct (apply t). can we do that?

Slide Q&A.

value_not_sae_as normal_form

e.g (1+2) + 7 e.g. 3 + 7

One-step

• plus
• left + 0
• right + 0

Inf-step -> Inf terms

go from 3 to 3+0

Stuck

No StepR

0 term can step into

Multi-Step Reduction ->*

1
2
3
4
5
6
Inductive multi {X : Type} (R : relation X) : relation X :=
| multi_refl : ∀(x : X), multi R x x
| multi_step : ∀(x y z : X),
R x y →
multi R y z →
multi R x z.


can be either defined as a “head + tail” style (or “tail + head” style), or “refl + trans” style (as in Rel.v).

the trans relation are underteministic in terms of the transtive relation using. (you can throw infinitely many trans constructors in)

having multiple form so we can jump back and forth to pick one easier for proof.

PLT PM lang

multiple smallstep relation can be markded deepner state.qjw er state.

IMP

astep no need for value

for If, in PLT we have 2 rules for T/F. here we can compute…

Par w/o Concurrency is deterministic (not vice versa)

suddenly / ->* /` tuple