形式陈述

小步操作语义给出配置之间的转移关系 $t\to t'$$t\to t^{\prime }$；其自反传递闭包记作 $\to^*$${\to }^{\ast }$。大步语义则直接定义求值关系 $t\Downarrow v$$t\Downarrow v$，表示项 $t$$t$ 运行得到值 $v$$v$。

直觉

它把编程语言规范写成一个抽象解释器：哪些表达式先算、一步之后变成什么，都由推导规则明确决定。

例子与边界

按值调用通常先把函数和实参求值，再执行 β-归约。操作语义描述执行行为，但不自动说明两个程序在所有上下文中是否等价。

推论与应用

确定性、终止性、类型安全和编译器正确性都可相对于操作语义精确定义和证明。

参考资料

• Gordon D. Plotkin, “A Structural Approach to Operational Semantics,” 1981.
• Benjamin C. Pierce, Types and Programming Languages, Chapters 3 and 5.