形式陈述

小步操作语义在配置集合 $\mathcal C$$\mathcal{C}$ 上给出一步转移关系

$$ \longrightarrow\ \subseteq\mathcal C\times\mathcal C. $$$$⟶\subseteq \mathcal{C}\times \mathcal{C}.$$

其反身传递闭包记为 $\longrightarrow^*$${⟶}^{\ast }$。若表达式配置为 $\langle e,\sigma\rangle$$⟨e,\sigma ⟩$，则

$$ \langle e,\sigma\rangle\longrightarrow^*\langle v,\sigma'\rangle $$$$⟨e,\sigma ⟩{⟶}^{\ast }⟨v,{\sigma }^{\prime }⟩$$

表示经过有限多个原子步骤得到值 $v$$v$ 与状态 $\sigma'$${\sigma }^{\prime }$。无限转移序列可表示发散；既不是终值又没有后继的配置称为 stuck。

直觉

小步语义像逐帧播放执行：每条规则只做一个局部动作，完整运行是这些动作的有限或无限链。它因此能显式观察中间状态、交错和控制转移。

例子与边界

对算术表达式，可有规则 $1+2\longrightarrow3$$1+2⟶3$，再由语境规则得到 $(1+2)+4\longrightarrow3+4$$(1+2)+4⟶3+4$。转移关系不必是函数：带随机选择、并发调度或非确定性运算的语言可从同一配置转向多个后继。反过来，确定性需要单独证明“每个配置至多一个后继”。

推论与应用

小步语义适合证明类型安全中的 preservation/progress、定义并发交错、追踪异常与资源成本。它与大步语义各有侧重：大步语义直接关联输入与终值，通常不自然表示发散和中间行为。

参考资料

• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Chs. 5–7。
• Gordon D. Plotkin, A Structural Approach to Operational Semantics, DAIMI FN-19, 1981; reprinted 2004，Full report, transition-system method。