Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment

TL;DR

This paper introduces a novel extension of big-step semantics, called big-stop semantics, which captures diverging computations without error states, combining the simplicity of big-step with the power of small-step semantics.

Contribution

It presents a simple, inductive extension to big-step semantics that accurately models divergence, avoiding complex rules and coinduction, demonstrated across various language variants.

Findings

Big-stop semantics captures divergence without error states.

The approach simplifies proofs and reasoning in Agda.

It applies to typed, untyped, and effectful languages.

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.