操作语义（小步/大步）

📖 什么叫”程序的含义”？

一个程序运行后会产生什么结果——这似乎不言自明。但精确地定义一个程序”是什么意思”，是编程语言理论的重要课题。

比如 x = x + 1——这句话”是什么意思”？不同语言可能有不同的理解：

• 在 C 中：从内存读取 x，加 1，写回内存
• 在 Haskell 中：x 没有被赋值（Haskell 没有赋值）——x 是一个定义
• 在 SQL 中：= 是比较，不是赋值

操作语义（Operational Semantics） 就是用”程序如何一步步执行”来精确描述程序的含义的数学方法。

🍳 类比：菜谱 vs 做菜的过程

菜谱：西红柿炒蛋的”定义”——“西红柿两个，鸡蛋三个……”

操作语义：你实际做菜的过程——

• 第 1 步：打三个鸡蛋到碗里
• 第 2 步：搅拌
• 第 3 步：切西红柿
• ……

“程序的含义”不是看菜谱上的文字，而是看实际操作步骤会产生什么结果。

---

👣 小步语义（Small-Step Semantics）——一步步来

小步语义描述程序”每一步”的变化——每次执行一个最原子的操作，然后进入下一个”状态”。

算术表达式的小步语义

(1 + 2) * (3 + 4)

第 1 步：先计算左边的 1+2
→ 3 * (3 + 4)

第 2 步：再计算右边的 3+4
→ 3 * 7

第 3 步：最后计算乘法
→ 21

用数学符号表示归约规则：

⟨n₁ + n₂, σ⟩ → ⟨n, σ⟩    如果 n = n₁ + n₂（两个数字相加）
⟨e₁ + e₂, σ⟩ → ⟨e₁' + e₂, σ⟩    如果 e₁ → e₁'（先归约左边）
⟨n₁ + e₂, σ⟩ → ⟨n₁ + e₂', σ⟩    如果 e₂ → e₂'（再归约右边）

这里 σ（sigma）表示状态——所有变量的当前值。

带变量的例子

# 考虑这段代码：
x = 1
y = x + 2

用状态 σ = {x → 1, y → ?} 表示：

执行过程：
⟨x + 2, {x → 1, y → ?}⟩     →   查找 x 在当前状态中的值
⟨1 + 2, {x → 1, y → ?}⟩     →   1+2 归约
⟨3, {x → 1, y → ?}⟩         →   结果 3，然后赋值给 y
{y → 3}                       →   更新状态

💡 小步语义的价值：你可以精确看到程序运行的”中间状态”——每一步发生了什么。这对于定义并发、异常处理等复杂特性特别有用。

---

🏃 大步语义（Big-Step Semantics）——直接到结果

大步语义不关心中间步骤——它直接把表达式”映射”到最终值：

⟨1+2, σ⟩ ⇓ 3
⟨3+4, σ⟩ ⇓ 7
──────────────────
⟨(1+2)*(3+4), σ⟩ ⇓ 21

横线上方是”前提”（子表达式的求值结果），横线下方是”结论”（整个表达式的求值结果）。

赋值语句的大步语义

⟨e, σ⟩ ⇓ v
──────────────────
⟨x = e, σ⟩ ⇓ σ[x → v]

意思是：如果表达式 e 在状态 σ 下求值得到 v，那么赋值语句 x = e 的结果是把状态更新为 σ[x → v]（把 x 的值设为 v）。

if-else 的大步语义

⟨e, σ⟩ ⇓ true    ⟨s₁, σ⟩ ⇓ σ'
──────────────────────────────
⟨if e then s₁ else s₂, σ⟩ ⇓ σ'

⟨e, σ⟩ ⇓ false    ⟨s₂, σ⟩ ⇓ σ'
──────────────────────────────
⟨if e then s₁ else s₂, σ⟩ ⇓ σ'

📐 形式语法：大步语义的每条规则是一个”推理规则”——如果”前提”都成立，那么”结论”成立。读者不需要理解每个数学符号的细节，只需知道它在描述”输入什么 → 得到什么”的映射。

---

⚔️ 小步 vs 大步——对比

维度	小步语义	大步语义
粒度	每次一步——细粒度	直接到最终值——粗粒度
中间状态	✅ 能描述	❌ 跳过中间状态
非终止程序	✅ 能处理（无限步骤）	❌ 无法表示（永不终止）
并发语义	✅ 自然支持（交错执行）	❌ 难以定义
证明程序性质	更复杂（步骤多）	更简洁（步骤少）

什么时候用哪个？

小步语义 → 为了研究"程序怎么执行"、并发、非确定性
大步语义 → 为了证明"程序性质"、类型安全、编译器正确性

实际上很多语言的定义两者都用：
- 小步：定义操作的"顺序"
- 大步：定义表达式的"求值"

---

🧩 操作语义的实际应用

定义新语言

# 假设你要设计一种新的小语言
# 操作语义就是它的"精确说明书"

# Lilliput 语言的语义（简化版）：

# 数值：⟨n, σ⟩ ⇓ n
# 加法：⟨e1, σ⟩ ⇓ v1, ⟨e2, σ⟩ ⇓ v2 → ⟨e1 + e2, σ⟩ ⇓ v1 + v2
# 变量：⟨x, σ⟩ ⇓ σ(x)          — 从状态中查找变量值
# 赋值：⟨e, σ⟩ ⇓ v → ⟨x = e, σ⟩ ⇓ σ[x → v]
# 序列：⟨s1, σ⟩ ⇓ σ', ⟨s2, σ'⟩ ⇓ σ'' → ⟨s1; s2, σ⟩ ⇓ σ''

证明类型安全

类型安全的证明通常使用操作语义：如果一个表达式”类型检查通过”，那么它的”操作语义执行不会卡住”（不会出现”类型错误”）。

类型安全定理：
如果 ⊢ e : τ（e 的类型为 τ）且 ⟨e, σ⟩ →* ⟨e', σ'⟩
那么要么 e' 是值，要么还有下一步 →*

通俗说：类型正确的程序不会"跑着跑着就炸了"

编译器正确性验证

编译器把高级语言翻译成机器码。怎么证明”翻译没有改变程序的含义”？

——用源语言和目标语言各自的操作语义，证明它们对同样的输入产生同样的结果。

---

📝 小结

概念	一句话
操作语义	用”程序怎么执行”来定义程序的含义
小步语义	每次归约一步——描述执行过程的每个中间状态
大步语义	从表达式直接到最终值——跳过中间步骤
状态（σ）	变量的当前值——执行环境的数学表示
归约规则	描述”表达式→新表达式”或”表达式⇓值”的规则
应用	语言定义、类型安全证明、编译器验证

🎯 思考题：考虑两个程序——一个无限循环（while True: pass），一个执行完就终止。在小步语义和大步语义中，这两个程序的”含义”分别如何表示？

为什么先学这个？ 操作语义是语言理论的”数学工具”。接下来看实际语言实现中的关键技术——垃圾回收机制。