大步语义推导树练习
大步语义描述了表达式或命令如何直接计算出最终结果或最终状态。推导树则通过逻辑规则的嵌套，清晰地展示了这一演化过程。
题目 1：算术表达式 Aexp
题目：在状态 $\sigma = \sigma_{init}[4/X][2/Y]$ 下，写出算术表达式 $(X + 1) \times Y$ 的执行推导过程。
答案：
$$\frac{\displaystyle \frac{\displaystyle \langle X, \sigma \rangle \to 4 \quad \langle 1, \sigma \rangle \to 1}{\langle X + 1, \sigma \rangle \to 5} \quad \langle Y, \sigma \rangle \to 2}{\langle (X + 1) \times Y, \sigma \rangle \to 10}$$
题目 2：布尔表达式 Bexp
题目：在状态 $\sigma = \sigma_{init}[3/X][5/Y]$ 下，写出布尔表达式 $\neg(X > 4) \wedge (Y = 5)$ 的执行推导过程。
答案：
$$\frac{\displaystyle \frac{\displaystyle \frac{\langle X, \sigma \rangle \to 3 \quad \langle 4, \sigma \rangle \to 4}{\langle X > 4, \sigma \rangle \to \text{false}}}{\langle \neg(X > 4), \sigma \rangle \to \text{true}} \quad \frac{\langle Y, \sigma \rangle \to 5 \quad \langle 5, \sigma \rangle \to 5}{\langle Y = 5, \sigma \rangle \to \text{true}}}{\langle \neg(X > 4) \wedge (Y = 5), \sigma \rangle \to \text{true}}$$
题目 3：综合命令 Com
题目：设初始状态 $\sigma = \sigma_{init}[1/X][0/Z]$，写出以下命令的完整推导树：
$X := 2; \text{if } X > 1 \text{ then } Z := X \text{ else } Z := 0$
答案：
为了书写清晰，记执行完第一条命令后的中间状态为 $\sigma_1 = \sigma[2/X]$，最终状态为 $\sigma’ = \sigma[2/X][2/Z]$。
$$\frac{\displaystyle \frac{\langle 2, \sigma \rangle \to 2}{\langle X := 2, \sigma \rangle \to \sigma_1} \quad \frac{\displaystyle \frac{\langle X, \sigma_1 \rangle \to 2 \quad \langle 1, \sigma_1 \rangle \to 1}{\langle X > 1, \sigma_1 \rangle \to \text{true}} \quad \frac{\langle X, \sigma_1 \rangle \to 2}{\langle Z := X, \sigma_1 \rangle \to \sigma’}}{\langle \text{if } X > 1 \text{ then } Z := X \text{ else } Z := 0, \sigma_1 \rangle \to \sigma’}}{\langle X := 2; \text{if } X > 1 \text{ then } Z := X \text{ else } Z := 0, \sigma \rangle \to \sigma’}$$
题目 4：复杂的 Aexp（多变量嵌套）
题目：在状态 $\sigma = \sigma_{init}[3/X][4/Y][2/Z]$ 下，写出算术表达式 $(X \times Y) - (Z + 1)$ 的推导树。
答案：
$$\frac{\displaystyle \frac{\langle X, \sigma \rangle \to 3 \quad \langle Y, \sigma \rangle \to 4}{\langle X \times Y, \sigma \rangle \to 12} \quad \frac{\langle Z, \sigma \rangle \to 2 \quad \langle 1, \sigma \rangle \to 1}{\langle Z + 1, \sigma \rangle \to 3}}{\langle (X \times Y) - (Z + 1), \sigma \rangle \to 9}$$
题目 5：复杂的 Bexp（逻辑组合与否定）
题目：在状态 $\sigma = \sigma_{init}[5/X][5/Y]$ 下，写出布尔表达式 $(X < 6) \wedge \neg(Y < 5)$ 的推导树。
答案：
$$\frac{\displaystyle \frac{\langle X, \sigma \rangle \to 5 \quad \langle 6, \sigma \rangle \to 6}{\langle X < 6, \sigma \rangle \to \text{true}} \quad \frac{\displaystyle \frac{\langle Y, \sigma \rangle \to 5 \quad \langle 5, \sigma \rangle \to 5}{\langle Y < 5, \sigma \rangle \to \text{false}}}{\langle \neg(Y < 5), \sigma \rangle \to \text{true}}}{\langle (X < 6) \wedge \neg(Y < 5), \sigma \rangle \to \text{true}}$$
题目 6：Com - 连续赋值（状态链传递）
题目：设 $\sigma = \sigma_{init}[0/X][0/Y]$，写出执行命令 $X := 3; Y := X + 2$ 的推导树。
注意：这考察的是第二个命令必须在第一个命令产生的“新状态”下执行。
答案：
记 $\sigma_1 = \sigma[3/X]$，最终状态为 $\sigma’ = \sigma[3/X][5/Y]$。
$$\frac{\displaystyle \frac{\langle 3, \sigma \rangle \to 3}{\langle X := 3, \sigma \rangle \to \sigma_1} \quad \frac{\displaystyle \frac{\langle X, \sigma_1 \rangle \to 3 \quad \langle 2, \sigma_1 \rangle \to 2}{\langle X + 2, \sigma_1 \rangle \to 5}}{\langle Y := X + 2, \sigma_1 \rangle \to \sigma’}}{\langle X := 3; Y := X + 2, \sigma \rangle \to \sigma’}$$
题目 7：Com - While 循环（2 次迭代）
题目：设 $\sigma = \sigma_{init}[1/X]$，写出执行命令 $\text{while } X < 3 \text{ do } X := X + 1$ 的推导树。
注意：While 的推导树是递归的。每一轮循环都会产生一个新的前提。
答案：
为了空间紧凑，记 $c \equiv X := X + 1$。
- 第一轮后状态 $\sigma_1 = \sigma[2/X]$
- 第二轮后状态 $\sigma_2 = \sigma[3/X]$
总推导树：
$$\frac{\displaystyle \langle X < 3, \sigma \rangle \to \text{true} \quad \frac{\langle X + 1, \sigma \rangle \to 2}{\langle c, \sigma \rangle \to \sigma_1} \quad \text{Tree_Iteration_2}}{\langle \text{while } X < 3 \text{ do } c, \sigma \rangle \to \sigma_2} \text{(W-T)}$$
其中 Tree_Iteration_2 (第二轮到结束) 为：
$$\frac{\displaystyle \langle X < 3, \sigma_1 \rangle \to \text{true} \quad \frac{\langle X + 1, \sigma_1 \rangle \to 3}{\langle c, \sigma_1 \rangle \to \sigma_2} \quad \frac{\langle X < 3, \sigma_2 \rangle \to \text{false}}{\langle \text{while } X < 3 \text{ do } c, \sigma_2 \rangle \to \sigma_2} \text{(W-F)}}{\langle \text{while } X < 3 \text{ do } c, \sigma_1 \rangle \to \sigma_2} \text{(W-T)}$$
