操作语义

操作语义把语言规范写成一台数学解释器。规则匹配当前配置的形状，前提描述子计算，结论给出下一配置或最终结果。推导树既是行为证据，也是证明确定性、模拟和类型保持时可归纳分析的对象。

与把程序组合地映到数学对象的指称语义理路指称语义Denotational semantics把程序构造组合地解释为数学对象与函数的语义方法。相比，操作语义直接保留执行结构，因此容易表达求值顺序、异常传播、状态更新与并发交错。一次语义步的粒度由规范者选择，不应未经成本对应证明就当作处理器指令。

以自然数和加法表达式为例，小步语义可用规则固定左到右顺序：

于是同一个表达式产生可观察的中间轨迹

大步语义不列出这些中间配置。取 $n\Downarrow n$ 为数值规则，再加入

直接推出

两套规则在这个终止、无错误片段上给出相同最终值，但提供的证据不同：小步轨迹记录中间项与顺序，大步推导组合子结果。大步规则把两个前提左右排开，并不单凭版面就规定时间先后；本例没有副作用，交换子计算也不改变结果。带状态的大步规则则应把第一个子计算的输出存储传给第二个子计算，显式落实顺序。

对应证明的一个方向是：假设大步推导的两个子树已经分别产生有限小步路径，先用左位置规则提升第一条路径，再用右位置规则提升第二条，最后执行一次加法。反方向可证明“一步化简不改变大步结果”，再沿小步路径归纳。这样得到的是全体项上的命题，不能由几个最终值相同的算例替代。

加入赋值后，配置必须携带存储，例如 $⟨e,\sigma ⟩$；否则 x := 1; x 的后半段无法观察前一步更新。异常若可捕获，控制栈或上下文也会影响传播位置。

必须区分三种未得到普通值的情形。true + 1 若既不是结果也没有规则，就是 stuck，可能代表非法程序或规范遗漏；若语言规定除零得到 error，则 $1/0\to \mathrm{error}$ 是显式行为；while true do skip 或 λ 项 $\mathrm{\Omega }$ 则不断有后继，属于 divergence。三者的可观察性要由语言规范决定。

公理语义理路公理语义Axiomatic semantics用逻辑断言和推理规则描述程序状态变换性质的语义方法。从另一角度用前置条件、后置条件和证明规则描述程序性质，不必列出执行步骤。操作规则可作为 Hoare 规则可靠性的参照，但两套语义承担不同职责。

小步语义理路小步操作语义Small-step operational semantics · Structural operational semantics用配置间的一步转移及有限或无限路径精确描述执行顺序、终止、卡住与发散。适合观察中间状态、并发交错和非终止，大步语义理路大步语义Big-step semantics · Natural semantics用表达式直接求值到最终结果的归纳判断描述程序执行。适合直接组织终止求值。二者只在明确值、错误和发散条件后才有可证明的对应命题。

求值上下文可集中描述允许计算的位置；在另行证明唯一分解后，确定求值才可表述为“寻找唯一 redex”。环境求值则常把函数值表示为代码与定义环境组成的闭包理路程序语言闭包Programming-language closure · Function closure · Lexical closure将函数代码与其定义位置的词法环境配对而成的运行时函数值。。按需调用理路按需调用与共享惰性求值Call by need · Shared lazy evaluation用 thunk 保存尚未执行的绑定，并在第一次强制求值后更新共享单元的非严格求值策略。与代数效应处理器理路代数效应与处理器Algebraic effect · Effect handler · Algebraic effects and handlers以操作签名表达效应，并由处理器解释返回值、操作参数及其受限恢复点的动态语义。会分别加入堆更新或 perform/handle 转移；这些实例扩展配置和规则，却仍使用同一语义接口。

在这套接口上，进展与保持定理理路进展与保持定理Progress and preservation · Type safety对按值调用的简单类型 lambda 演算逐层解释规范形、替换、进展与保持，以及类型安全的准确结论。把类型判断与执行步骤联系起来；程序等价和编译器正确性则比较两套关系是否保持可观察行为。它们需要先固定语义，不能反过来代替动态规则。

面向程序分析时，控制流图理路控制流图Control-flow graph · Program control-flow graph以基本块或程序点为节点、以可能的执行转移为边表示过程内控制流的有向图。提取可能的控制转移，收集语义理路收集语义Collecting semantics · Reachability semantics at program points为每个程序点收集所有可达具体状态，作为静态分析需要可靠逼近的具体语义基准。在各程序点汇总操作语义可达的具体状态，抽象机器理路抽象机器Abstract machine · Operational abstract machine把程序执行写成显式配置与局部转移规则，并通过解码或模拟关系连接源语言语义的操作模型。则把控制、环境和存储显式化为可执行配置。它们分别是结构投影、语义汇总和执行模型；模型检查或抽象解释算法在这些对象上工作，但语义步数仍不自动等于机器运行成本。