形式陈述

大步语义用归纳判断 $e\Downarrow v$$e\Downarrow v$ 表示表达式 $e$$e$ 经完整求值得到值 $v$$v$。规则直接组合子表达式的最终结果，例如应用规则先推导函数与参数结果，再推导函数体结果。普通归纳大步语义只描述终止执行；发散需要共归纳关系、燃料参数或与小步语义联合刻画。

直觉

它把许多机器小步压成一棵求值证明树，关注输入表达式与最终结果之间的关系。

例子与边界

算术表达式规则可从 $e_1\Downarrow n_1,e_2\Downarrow n_2$$e_1\Downarrow n_1,e_2\Downarrow n_2$ 推出 $e_1+e_2\Downarrow n_1+n_2$$e_1+e_2\Downarrow n_1+n_2$。没有推导既可能表示发散，也可能表示卡住，除非语言另有类型安全或错误语义。并发中的中间交错通常不能仅靠简单大步关系表达。

推论与应用

大步语义适合解释器、编译器正确性和自然语义证明；小步语义则更适合观察中间状态、并发和控制效果。

参考资料

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