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

Small-step semantics and big-step semantics are two styles for

operationally dening the meaning of programming languages. Small-step

semantics are given as a relation between program congurations that

denotes one computational step; big-step semantics are given as a relation

directly associating to each program conguration the corresponding

nal conguration. 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

dene 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 identied assumptions are met, it is sound

and complete in the sense that the two semantics are equivalent. For a

strict subset of the identied assumptions, we show that the resulting

big-step semantics is sound but not necessarily complete. We discuss our

transformation on a number of examples.