Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
David M Kahn, Jan Hoffmann, Runming Li
TL;DR
This work addresses the limitation of standard big-step semantics in describing nonterminating computations by introducing big-stop semantics, an inductive extension that adds a single nondeterministic stopping rule to capture finite prefixes of potentially infinite computations. It demonstrates that big-stop semantics is equivalent to the reflexive-transitive closure of small-step evaluation and shows how it preserves the ergonomic benefits of big-step proofs while enabling rigorous reasoning about divergence. The approach is instantiated for call-by-value PCF (typed, untyped, and effectful) and an imperative language, with formal proofs and Agda mechanizations highlighting its practical usability. The paper also presents the big-stop method as a systematic strategy for extending terminating theorems to diverging ones, along with ergonomic optimizations (normal forms, evaluation contexts, annihilator effects) and an imperative variant, illustrating broad applicability to compiler correctness and verification tasks. Overall, big-stop semantics offers a simple, inductive, and scalable path to combining the intuitiveness of big-step reasoning with the power to model divergence, with tangible benefits for semantic preservation and verification workflows.
Abstract
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.