A big-step operational semantics relates an expression directly to its final result, skipping intermediate machine states.

A judgment

$$e\Downarrow v$$

means that expression $e$ evaluates to value $v$.

For function application in a call-by-value language, a rule can say: evaluate the function expression to a function value, evaluate the argument to a value, then evaluate the function body with the parameter bound to that argument value. The premises describe the complete evaluations needed to justify the conclusion.

For arithmetic,

$$\frac{e_1\Downarrow n_1\qquad e_2\Downarrow n_2}{e_1+e_2\Downarrow n_1+n_2}.$$

Big-step rules are often concise and close to the recursive structure of an interpreter. They answer “what result does this program produce?” without representing each execution step.

The trade-off is that plain big-step semantics does not naturally distinguish several ways of failing to produce a result: divergence, getting stuck and some runtime errors can all correspond to the absence of a derivation. Small-step semantics exposes these distinctions more directly.

The two styles are complementary descriptions of language behavior, and for well-behaved terminating programs they can often be proved equivalent.