小步操作语义 | Codeboy's Blog

形式陈述

小步操作语义以配置上的二元关系 $C\to C'$ 表示一个抽象计算步骤。有限执行由自反传递闭包 $\to^*$ 给出，无限执行是序列 $C_0\to C_1\to\cdots$ 。

语义还必须指定值集合 $\mathrm{Val}$ 。由小步关系导出的正常求值可记为

e\Downarrow_{\to}v \iff e\to^*v\land v\in\mathrm{Val}.

下标用于区分这个派生结果关系与原始大步判断。若语言有显式错误，再指定终止错误集合 $\mathrm{Err}$ 以及相应传播规则；错误可达写成

e\Downarrow_{\to}\mathrm{error} \iff \exists e_{\mathrm{err}}\in\mathrm{Err},\ e\to^*e_{\mathrm{err}}.

无后继且既不是值也不是显式错误的配置称为 stuck。因此“ $e\not\to$ ”只表示不可继续，必须再检查终态分类。一个小步语义是确定的，若

C\to C_1\land C\to C_2 \Longrightarrow C_1=C_2.

规则通常分成计算规则与位置规则：前者收缩 redex，后者把子项步骤提升到外层。位置规则也可由求值上下文统一写成 $E[r]\to E[r']$ 。值、redex 和上下文文法共同决定求值策略。

直觉

小步语义把执行展开成路径，每一步只兑现一个局部规则。中间状态让求值顺序、异常传播和并发交错成为模型的一部分；无限路径则直接见证发散。

同一组根计算规则可以配上不同上下文文法，形成调用值、调用名或其他策略。策略差异不需要改写 β-收缩本身，只需改变允许暴露哪个 redex。

例子与边界

在左到右整数表达式语义中，

(1+2)\times(3+4)\to3\times(3+4)\to3\times7\to21.

每一步都只化简当前最左可求值子式。对 λ 项，令 $\Omega=(\lambda z.z\,z)(\lambda z.z\,z)$ 。调用值语义先把函数与实参都求成值；调用名可直接收缩外层应用，因此

(\lambda x.0)\Omega

在调用值下发散，在调用名下走一步得到 $0$ 。两种行为都来自完整 β-归约的子关系，差异由策略选择造成。

若 true + 1 不是值、错误且没有规则，它是 stuck；若 $\Omega$ 每步都回到自身，它发散。两者都没有正常结果，却有完全不同的路径形状。开项 $x$ 也可能无步可走，因此进展定理通常要求闭项。

小步关系不必确定。并发线程任一方都可先执行，非确定语言也可保留多个合法后继。顺序语言若声称确定，则应通过规则互斥或唯一分解证明每个非终态至多暴露一个 redex。

推论与应用

小步语义适合类型安全证明：进展说明良类型闭项要么是规定结果、要么还能走一步；保持说明每一步延续类型判断。安全不变量可沿路径长度归纳，发散则由无限转移序列描述。

并发语义、抽象机器和编译器模拟都以小步关系为自然接口。给转移补上可观察动作可得到标号转移系统，再由轨迹与路径语义解释完整运行；时序规格与模型检查算法建立在这套语义对象之上，但不是小步规则本身。

机器把控制、环境、存储或续延显式放进配置，并通过解码关系与源小步语义建立模拟。与大步语义比较时，通常先证明终止程序的结果对应，再单独处理错误与发散；小步额外保留中间行为。

参考资料

Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016, Chapters 5–7。
Gordon D. Plotkin, “A Structural Approach to Operational Semantics,” DAIMI FN-19, 1981; reprinted in Journal of Logic and Algebraic Programming 60–61, 2004。
Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002, Chapters 3 and 8。