等价性证明练习
在形式语义学的研究中，证明两个程序片段在语义上等价（$c_1 \sim c_2$）是一项基础工作。这意味着对于任何初始状态 $\sigma$ 和结束状态 $\sigma’$，$\langle c_1, \sigma \rangle \to \sigma’$ 当且仅当 $\langle c_2, \sigma \rangle \to \sigma’$。
以下是几个典型等价性的证明。
1. 证明：$c; \text{skip} \sim c$
方向 1：[$\Rightarrow$]
假设 $\langle c; \text{skip}, \sigma \rangle \to \sigma’$。
根据顺序执行规则 (Seq)，必然存在状态 $\sigma’’$，使得推导树如下：
$$\frac{\langle c, \sigma \rangle \to \sigma’’ \quad \langle \text{skip}, \sigma’’ \rangle \to \sigma’}{\langle c; \text{skip}, \sigma \rangle \to \sigma’} \text{(Seq)}$$
根据 skip 命令的规则：$\langle \text{skip}, \sigma’’ \rangle \to \sigma’’$。
因此必须有 $\sigma’ = \sigma’’$。
将 $\sigma’ = \sigma’’$ 代入前提条件的左侧，得到 $\langle c, \sigma \rangle \to \sigma’$。
方向 2：[$\Leftarrow$]
假设 $\langle c, \sigma \rangle \to \sigma’$。
根据 skip 命令的规则，在状态 $\sigma’$ 下有：$\langle \text{skip}, \sigma’ \rangle \to \sigma’$。
根据顺序执行规则 (Seq)，可以构造推导树：
$$\frac{\langle c, \sigma \rangle \to \sigma’ \quad \langle \text{skip}, \sigma’ \rangle \to \sigma’}{\langle c; \text{skip}, \sigma \rangle \to \sigma’} \text{(Seq)}$$
2. 证明：$\text{if } b \text{ then } c \text{ else } c \sim c$
方向 1：[$\Rightarrow$]
假设 $\langle \text{if } b \text{ then } c \text{ else } c, \sigma \rangle \to \sigma’$。
根据 if 的规则，存在两种情况：
- Case 1: $\langle b, \sigma \rangle \to \text{true}$
此时推导树必定为：
$$\frac{\langle b, \sigma \rangle \to \text{true} \quad \langle c, \sigma \rangle \to \sigma’}{\langle \text{if } b \text{ then } c \text{ else } c, \sigma \rangle \to \sigma’} \text{(IF-T)}$$
从中可以直接提取出 $\langle c, \sigma \rangle \to \sigma’$。 - Case 2: $\langle b, \sigma \rangle \to \text{false}$
此时推导树必定为：
$$\frac{\langle b, \sigma \rangle \to \text{false} \quad \langle c, \sigma \rangle \to \sigma’}{\langle \text{if } b \text{ then } c \text{ else } c, \sigma \rangle \to \sigma’} \text{(IF-F)}$$
从中也可以直接提取出 $\langle c, \sigma \rangle \to \sigma’$。
方向 2：[$\Leftarrow$]
假设 $\langle c, \sigma \rangle \to \sigma’$。
在状态 $\sigma$ 下，布尔表达式 $b$ 只有两种可能的取值：
- Case 1: $\langle b, \sigma \rangle \to \text{true}$
构造推导树：
$$\frac{\langle b, \sigma \rangle \to \text{true} \quad \langle c, \sigma \rangle \to \sigma’}{\langle \text{if } b \text{ then } c \text{ else } c, \sigma \rangle \to \sigma’} \text{(IF-T)}$$ - Case 2: $\langle b, \sigma \rangle \to \text{false}$
构造推导树：
$$\frac{\langle b, \sigma \rangle \to \text{false} \quad \langle c, \sigma \rangle \to \sigma’}{\langle \text{if } b \text{ then } c \text{ else } c, \sigma \rangle \to \sigma’} \text{(IF-F)}$$
3. 证明：$\text{while false do } c \sim \text{skip}$
方向 1：[$\Rightarrow$]
假设 $\langle \text{while false do } c, \sigma \rangle \to \sigma’$。
由于循环条件始终为 false，只能采用 While-F 规则，推导树如下：
$$\frac{\langle \text{false}, \sigma \rangle \to \text{false}}{\langle \text{while false do } c, \sigma \rangle \to \sigma} \text{(While-F)}$$
由此可知 $\sigma’ = \sigma$。
根据 skip 规则，已知 $\langle \text{skip}, \sigma \rangle \to \sigma$，由于 $\sigma’ = \sigma$，所以 $\langle \text{skip}, \sigma \rangle \to \sigma’$。
方向 2：[$\Leftarrow$]
假设 $\langle \text{skip}, \sigma \rangle \to \sigma’$。
根据 skip 规则，必有 $\sigma’ = \sigma$。
构造 while 的推导树：
$$\frac{\langle \text{false}, \sigma \rangle \to \text{false}}{\langle \text{while false do } c, \sigma \rangle \to \sigma} \text{(While-F)}$$
由于 $\sigma’ = \sigma$，结论即为 $\langle \text{while false do } c, \sigma \rangle \to \sigma’$。
4. 证明：$((\text{if } b \text{ then } c_1 \text{ else } c_2); c_3) \sim (\text{if } b \text{ then } (c_1; c_3) \text{ else } (c_2; c_3))$
方向 1：[$\Rightarrow$]
假设 $\langle (\text{if } b \text{ then } c_1 \text{ else } c_2); c_3, \sigma \rangle \to \sigma’$。
由顺序执行规则，存在 $\sigma’’$ 使得：$\langle \text{if } b \text{ then } c_1 \text{ else } c_2, \sigma \rangle \to \sigma’’$ 且 $\langle c_3, \sigma’’ \rangle \to \sigma’$。
- Case 1: $\langle b, \sigma \rangle \to \text{true}$
左侧推导树如下：
$$\frac{\frac{\langle b, \sigma \rangle \to \text{true} \quad \langle c_1, \sigma \rangle \to \sigma’’}{\langle \text{if } b \text{ then } c_1 \text{ else } c_2, \sigma \rangle \to \sigma’’} \text{(IF-T)} \quad \langle c_3, \sigma’’ \rangle \to \sigma’}{\langle (\text{if } b \text{ then } c_1 \text{ else } c_2); c_3, \sigma \rangle \to \sigma’} \text{(Seq)}$$
利用已知条件构造右侧：
$$\frac{\langle b, \sigma \rangle \to \text{true} \quad \frac{\langle c_1, \sigma \rangle \to \sigma’’ \quad \langle c_3, \sigma’’ \rangle \to \sigma’}{\langle c_1; c_3, \sigma \rangle \to \sigma’} \text{(Seq)}}{\langle \text{if } b \text{ then } (c_1; c_3) \text{ else } (c_2; c_3), \sigma \rangle \to \sigma’} \text{(IF-T)}$$ - Case 2: $\langle b, \sigma \rangle \to \text{false}$
（同理构造，将 $c_1$ 替换为 $c_2$ 并使用If-F规则）。
方向 2：[$\Leftarrow$]
（思路完全对称，仅需将上述推导树的构造顺序反转即可）。
5. 证明：$\text{while } b \text{ do } c \sim (\text{while } b \text{ do } c); (\text{while } b \text{ do } c)$
方向 1：[$\Rightarrow$]
假设 $\langle \text{while } b \text{ do } c, \sigma \rangle \to \sigma’$。
循环能够终止到 $\sigma’$，根据 while 语义，此时布尔表达式 $b$ 在结束状态必须满足：$\langle b, \sigma’ \rangle \to \text{false}$。
根据 While-F 规则，我们可以得到：
$$\frac{\langle b, \sigma’ \rangle \to \text{false}}{\langle \text{while } b \text{ do } c, \sigma’ \rangle \to \sigma’} \text{(While-F)}$$
现在构造右侧的顺序执行推导树：
$$\frac{\langle \text{while } b \text{ do } c, \sigma \rangle \to \sigma’ \quad \frac{\langle b, \sigma’ \rangle \to \text{false}}{\langle \text{while } b \text{ do } c, \sigma’ \rangle \to \sigma’} \text{(While-F)}}{\langle (\text{while } b \text{ do } c); (\text{while } b \text{ do } c), \sigma \rangle \to \sigma’} \text{(Seq)}$$
方向 2：[$\Leftarrow$]
假设 $\langle (\text{while } b \text{ do } c); (\text{while } b \text{ do } c), \sigma \rangle \to \sigma’$。
根据 Seq 规则，存在 $\sigma’’$ 使得：
$\langle \text{while } b \text{ do } c, \sigma \rangle \to \sigma’’$ 且 $\langle \text{while } b \text{ do } c, \sigma’’ \rangle \to \sigma’$。
因为第一个循环已执行完毕，必有：$\langle b, \sigma’’ \rangle \to \text{false}$。
根据 While-F 规则，第二个循环的执行必定是：
$$\frac{\langle b, \sigma’’ \rangle \to \text{false}}{\langle \text{while } b \text{ do } c, \sigma’’ \rangle \to \sigma’’} \text{(While-F)}$$
由于前提已知第二个循环到达 $\sigma’$，所以 $\sigma’ = \sigma’’$。
代入第一个循环的结论，得到 $\langle \text{while } b \text{ do } c, \sigma \rangle \to \sigma’$。
6. 证明：$\text{while } b \text{ do } c \sim \text{while } b \text{ do } (\text{if } b \text{ then } c \text{ else skip})$
(注：此类涉及 while 且两边命令不完全一致的题目，严谨证明需对推导树高度 $n$ 进行归纳)
方向 1：[$\Rightarrow$]
假设 $\langle \text{while } b \text{ do } c, \sigma \rangle \to \sigma’$。对推导树高度归纳：
- 基准步骤 (While-F): $\langle b, \sigma \rangle \to \text{false}$。
右边：$\frac{\langle b, \sigma \rangle \to \text{false}}{\langle \text{while } \dots, \sigma \rangle \to \sigma}$，成立。 - 归纳步骤 (While-T): $\langle b, \sigma \rangle \to \text{true}$ 且 $\langle c, \sigma \rangle \to \sigma’’$ 且 $\langle \text{while } b \text{ do } c, \sigma’’ \rangle \to \sigma’$。
我们要为右侧构造推导树。首先看内部的if：
$$\frac{\langle b, \sigma \rangle \to \text{true} \quad \langle c, \sigma \rangle \to \sigma’’}{\langle \text{if } b \text{ then } c \text{ else skip}, \sigma \rangle \to \sigma’’} \text{(IF-T)}$$
整体右侧推导树：
$$\frac{\langle b, \sigma \rangle \to \text{true} \quad \langle \text{if } \dots, \sigma \rangle \to \sigma’’ \quad \langle \text{while } \dots, \sigma’’ \rangle \to \sigma’}{\langle \text{while } b \text{ do } (\text{if } b \text{ then } c \text{ else skip}), \sigma \rangle \to \sigma’} \text{(While-T)}$$
(第三个前提由归纳假设成立)
方向 2：[$\Leftarrow$]
（同理，通过归纳法，观察到当 $b$ 为 true 时，if b then c else skip 恒等价于执行 $c$）。
