小步语义格局变换练习
在小步语义中，我们关注程序执行的每一步演化。一个格局通常表示为 $\langle c, \sigma \rangle$（命令与状态对）或直接是一个状态 $\sigma$（在非变种语义中表示终止）。
以下是针对不同表达式和语句的格局变换练习汇总。
一、 算术表达式 Aexp 与布尔表达式 Bexp
题目 1：算术表达式 Aexp 归约
题目：假设 $\sigma(X) = 4$，写出 $\langle (X + 2) \times (3 - 1), \sigma \rangle$ 的小步语义格局变换。
答案：
$\langle (X + 2) \times (3 - 1), \sigma \rangle$
$\to_1 \langle (4 + 2) \times (3 - 1), \sigma \rangle$ （变量替换）
$\to_1 \langle 6 \times (3 - 1), \sigma \rangle$ （计算左侧括号）
$\to_1 \langle 6 \times 2, \sigma \rangle$ （计算右侧括号）
$\to_1 \langle 12, \sigma \rangle$ （最终求值）
题目 2：Bexp 独立归约过程
题目：假设 $\sigma(X) = 3, \sigma(Y) = 5$，写出布尔表达式 $\neg(X < 2) \wedge (Y = 5)$ 的小步语义格局变换。
答案：
$\langle \neg(X < 2) \wedge (Y = 5), \sigma \rangle$
$\to_1 \langle \neg(3 < 2) \wedge (Y = 5), \sigma \rangle$ （变量替换 X）
$\to_1 \langle \neg \text{false} \wedge (Y = 5), \sigma \rangle$ （计算比较运算）
$\to_1 \langle \text{true} \wedge (Y = 5), \sigma \rangle$ （处理否定 $\neg$）
$\to_1 \langle \text{true} \wedge (5 = 5), \sigma \rangle$ （变量替换 Y）
$\to_1 \langle \text{true} \wedge \text{true}, \sigma \rangle$ （计算等于运算）
$\to_1 \text{true}$ （最终 Bexp 的值）
二、 命令语句 Com（非变种模式）
注：非变种模式下，赋值语句的最后一步直接归约至状态 $\sigma$。
题目 1：基础顺序执行
题目：设 $\sigma$ 为初始状态，写出命令 $X := 1 + 2; Y := X \times 2$ 的小步语义格局变换。
答案：
$\langle X := 1 + 2; Y := X \times 2, \sigma \rangle$
$\to_1 \langle X := 3; Y := X \times 2, \sigma \rangle$ （计算第一个赋值右侧）
$\to_1 \langle Y := X \times 2, \sigma[3/X] \rangle$ （非变种：完成第一个赋值，进入下一条命令）
$\to_1 \langle Y := 3 \times 2, \sigma[3/X] \rangle$ （变量替换）
$\to_1 \langle Y := 6, \sigma[3/X] \rangle$ （计算第二个赋值右侧）
$\to_1 \sigma[3/X][6/Y]$ （最终终止状态为 $\sigma$）
题目 2：带有复杂计算的顺序执行
题目：设 $\sigma(X) = 0$，写出 $X := X + 1; X := X + 2$ 的非变种小步语义格局变换。
答案：
$\langle X := X + 1; X := X + 2, \sigma \rangle$
$\to_1 \langle X := 0 + 1; X := X + 2, \sigma \rangle$
$\to_1 \langle X := 1; X := X + 2, \sigma \rangle$
$\to_1 \langle X := X + 2, \sigma[1/X] \rangle$
$\to_1 \langle X := 1 + 2, \sigma[1/X] \rangle$
$\to_1 \langle X := 3, \sigma[1/X] \rangle$
$\to_1 \sigma[1/X][3/X]$ （也可写为 $\sigma[3/X]$）
三、 命令语句 Com（变种模式）
注：变种模式下，所有命令最终都归约至 $\langle \text{skip}, \sigma \rangle$。
题目 1：基础赋值变换
题目：设 $\sigma$ 为初始状态，写出命令 $X := 5; Y := 1$ 的变种小步语义格局变换。
答案：
$\langle X := 5; Y := 1, \sigma \rangle$
$\to_1 \langle \text{skip}; Y := 1, \sigma[5/X] \rangle$ （变种：赋值先产生 skip）
$\to_1 \langle Y := 1, \sigma[5/X] \rangle$ （skip 规则：消除序列左侧的 skip）
$\to_1 \langle \text{skip}, \sigma[5/X][1/Y] \rangle$ （最终终止于 $\langle \text{skip}, \sigma \rangle$）
题目 2：If 分支语句（变种模式）
题目：假设 $\sigma(X) = 2$，写出命令 $\text{if } X > 1 \text{ then } Y := 1 \text{ else } Y := 0$ 的变种变换。
答案：
$\langle \text{if } X > 1 \text{ then } Y := 1 \text{ else } Y := 0, \sigma \rangle$
$\to_1 \langle \text{if } 2 > 1 \text{ then } Y := 1 \text{ else } Y := 0, \sigma \rangle$ （变量替换）
$\to_1 \langle \text{if true then } Y := 1 \text{ else } Y := 0, \sigma \rangle$ （布尔求值）
$\to_1 \langle Y := 1, \sigma \rangle$ （If-True 选择分支）
$\to_1 \langle \text{skip}, \sigma[1/Y] \rangle$ （变种赋值终止）
题目 3：While 循环的展开（变种模式）
题目：假设 $\sigma(X) = 2$，写出命令 $\text{while } X = 2 \text{ do } X := 0$ 的变换前几步。
注意：While 的第一步是展开为 If 语句。
答案：
$\langle \text{while } X = 2 \text{ do } X := 0, \sigma \rangle$
$\to_1 \langle \text{if } X = 2 \text{ then } (X := 0; \text{while } X = 2 \text{ do } X := 0) \text{ else skip}, \sigma \rangle$ （While 展开规则）
$\to_1 \langle \text{if } 2 = 2 \text{ then } (X := 0; \text{while } X = 2 \text{ do } X := 0) \text{ else skip}, \sigma \rangle$ （变量替换）
$\to_1 \langle \text{if true then } (X := 0; \text{while } X = 2 \text{ do } X := 0) \text{ else skip}, \sigma \rangle$ （Bexp 求值）
$\to_1 \langle X := 0; \text{while } X = 2 \text{ do } X := 0, \sigma \rangle$ （If-True 选择）
$\to_1 \langle \text{skip}; \text{while } X = 2 \text{ do } X := 0, \sigma[0/X] \rangle$ （赋值产生 skip）
$\to_1 \langle \text{while } X = 2 \text{ do } X := 0, \sigma[0/X] \rangle$ （消除序列开头的 skip）
（后续会再次进入 While 展开，并因为 $0 = 2$ 为 false 而终止）
四、 综合复杂练习
多变量与逻辑与（非变种模式）
题目：设 $\sigma = \sigma_{init}[2/X][2/Y]$，写出命令 $Z := 0; \text{if } X = Y \wedge Y = 2 \text{ then } Z := 1$ 的变换过程。
答案：
$\langle Z := 0; \text{if } X = Y \wedge Y = 2 \text{ then } Z := 1, \sigma \rangle$
$\to_1 \langle \text{if } X = Y \wedge Y = 2 \text{ then } Z := 1, \sigma[0/Z] \rangle$ （完成第一个赋值）
$\to_1 \langle \text{if } 2 = Y \wedge Y = 2 \text{ then } Z := 1, \sigma[0/Z] \rangle$ （If 条件内部：替换 X）
$\to_1 \langle \text{if } 2 = 2 \wedge Y = 2 \text{ then } Z := 1, \sigma[0/Z] \rangle$ （If 条件内部：替换 Y）
$\to_1 \langle \text{if true} \wedge Y = 2 \text{ then } Z := 1, \sigma[0/Z] \rangle$ （计算第一个等于）
$\to_1 \langle \text{if true} \wedge 2 = 2 \text{ then } Z := 1, \sigma[0/Z] \rangle$ （继续替换 Y）
$\to_1 \langle \text{if true} \wedge \text{true then } Z := 1, \sigma[0/Z] \rangle$ （计算第二个等于）
$\to_1 \langle \text{if true then } Z := 1, \sigma[0/Z] \rangle$ （逻辑与计算）
$\to_1 \langle Z := 1, \sigma[0/Z] \rangle$ （If-True 选择）
$\to_1 \sigma[0/Z][1/Z]$ （最终终止状态）
