As is evident in the programming language literature, many practitioners favor specifying dynamic program behavior using big-step over small-step semantics. Unlike small-step semantics, which must dwell on every intermediate program state, big-step semantics conveniently jumps directly to the ever-important result of the computation. Big-step semantics also typically involves fewer inference rules than their small-step counterparts. However, in exchange for ergonomics, big-step semantics gives up power: Small-step semantics describes program behaviors that are outside the grasp of big-step semantics, notably divergence. This work presents a little-known extension of big-step semantics with inductive definitions that captures diverging computations without introducing error states. This big-stop semantics is illustrated for typed, untyped, and effectful variants of PCF, as well as a while-loop-based imperative language. Big-stop semantics extends the standard big-step inference rules with a few additional rules to define an evaluation judgment that is equivalent to the reflexive-transitive closure of small-step transitions. This simple extension contrasts with other solutions in the literature that sacrifice ergonomics by introducing many additional inference rules, global state, and/or less-commonly-understood reasoning principles like coinduction. The ergonomics of big-stop semantics is exemplified via concise Agda proofs for some key results and compilation theorems.

翻译：正如编程语言文献中所明确体现的，许多实践者倾向于使用大步语义而非小步语义来规定程序的动态行为。与小步语义必须详述每个中间程序状态不同，大步语义能便捷地直接跳转至计算中至关重要的最终结果。大步语义通常也比对应的小步语义涉及更少的推理规则。然而，为了换取这种易用性，大步语义牺牲了表达能力：小步语义能够描述大步语义无法捕捉的程序行为，特别是发散（divergence）。本文提出了一种鲜为人知的大步语义扩展，它通过归纳定义来捕获发散计算，而无需引入错误状态。这种大停止语义通过类型化、无类型化及带效应的PCF变体，以及一个基于while循环的命令式语言进行了阐释。大停止语义在标准大步推理规则的基础上，增加了少量额外规则，从而定义了一个等价于小步转换的自反传递闭包的求值判定。这种简单的扩展与文献中其他牺牲易用性的解决方案形成对比，后者通过引入大量额外的推理规则、全局状态和/或较不常见的推理原则（如共归纳）来实现。大停止语义的易用性通过一些关键结果和编译定理的简洁Agda证明得到了例证。