大步语义

大步语义像一个递归解释器的规格：先求子表达式的结果，再组合成整体结果，中间小步骤不进入判断。它让“这个程序算出什么”非常直接，也使按语法结构证明性质较为简洁。代价是路径被压缩掉了：两个以相同值结束但求值顺序不同的程序可能得到同一个判断。更关键的是，在普通归纳大步语义中，发散和卡住都表现为“无法构造推导”，需要额外机制才能区分。

对 $1+(2\times 3)$，先用乘法规则得到 $2\times 3\Downarrow 6$，再用加法规则得到 $1+6\Downarrow 7$，整次计算由一棵有限推导树表示。有存储时，规则必须把前一个子表达式产生的存储传给后一个子表达式，才能刻画副作用顺序。

边界例子是无限循环与类型错误：在最朴素的大步语义中，while true do skip 与 1 true 都没有 $e\Downarrow v$ 的推导，一个是发散，一个是卡住。可另用共归纳定义 $e\Uparrow$、加入显式错误结果，或用燃料参数补足这一区分；共归纳发散判断是与有限求值推导配套的另一关系，不是把一棵无限证明树直接当成普通 $e\Downarrow v$。大步语义也不适合直接枚举并发执行的每个交错步骤。

大步语义常用于定义解释器、常量求值和表达式语言的参考规范。证明算法正确性公理库算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。时，可对求值推导树归纳；编译器正确性也常陈述为源程序与目标程序的大步结果一致。

与小步语义公理库小步操作语义Small-step operational semantics · Structural operational semantics用配置间的一步转移及有限或无限路径精确描述执行顺序、终止、卡住与发散。的对应关系是重要校验：对终止程序，通常证明 $e\Downarrow v$ 当且仅当 $e{\to }^{\ast }v$。异常和状态可通过扩展结果与配置自然纳入，但非终止行为需单独处理。

由于大步判断压掉中间配置，它适合证明输入—结果关系，却不能直接提供轨迹语义公理库轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。所需的逐步路径；检查中间安全状态、并发交错或时序性质时，通常先选小步转移系统，再运行模型检查或抽象解释算法。