From Small-step Semantics to Big-step Semantics, Automatically

Small-step semantics and big-step semantics are two styles for
operationally defining the meaning of programming
languages. Small-step semantics are given as a relation between
program configurations that denotes one computational step; big-step
semantics are given as a relation directly associating to each program
configuration the corresponding final configuration. Small-step
semantics are useful for making precise reasonings about programs, but
reasoning in big-step semantics is easier and more intuitive. When
both small-step and big-step semantics are needed for the same
language, a proof of the fact that the two semantics are equivalent
should also be provided in order to trust that they both define the
same language. We show that the big-step semantics can be
automatically obtained from the small-step semantics when the
small-step semantics are given by inference rules satisfying certain
assumptions that we identify. The transformation that we propose is
very simple and we show that when the identified assumptions are met,
it is sound and complete in the sense that the two semantics are
equivalent. For a strict subset of the identified assumptions, we show
that the resulting big-step semantics is sound but not necessarily
complete. We discuss our transformation on a number of examples.

Sidebar