Difference Between Small and Big-step Operational Semantics

Small-step semantics defines a method to evaluate expressions one computation step at a time. Formally speaking, a small-step semantics for an expression language $E$ is a relation $rightarrow : E times E$ called the reduction relation. Small-step semantics describes what happens to an expression in detail. It’s able to give a precise account of even non-terminating programs, with an infinite chain $e_0 to e_1 to e_2 to dots$. A terminating program is one such that $e_0 to e_1 to dots to v$ terminates with a value $v$ such that $forall e’ in E, v notrightarrow e’$. $newcommand{llbracket}{[![} newcommand{rrbracket}{]!]}$ At the other end of the spectrum is denotational semantics. Denotational semantics assigns a “meaning” to each expression. It is a function from expressions to denotations: $llbracket cdot rrbracket : E to D$ ($D$ is called the domain). The space of denotations can be completely unrelated to the syntactic space, for example $E$ could be expressions that evaluated to a number and $D$ could be a set of numbers like $mathbb{N}$ or $mathbb{R}$. Big-step semantics are kind of in the middle. A big-step semantics on an expression language $E$ and a set of values $V$ is a relation $Downarrow : E times V$. It relates an expression to its value (possibly multiple values if the language is non-deterministic). Often, a special value $bot$ is used for non-terminating expressions. So why do we have these three notions? All of these notions can model each other, but the model adds a degree of complexity.

• Given a small-step semantics $to$, you can define a corresponding big-step semantics that relates each expression to its value (or values, if the reduction is non-deterministic): $e Downarrow v$ iff there exists a chain $e to e_1 to dots to v$ and $v$ cannot reduce any further. Note that in general you cannot reconstruct the small-step semantics from the big-step semantics. For example, all non-terminating expressions are indistinguishable under the big-step semantics.
• Given a big-step semantics $Downarrow : E times V$, you can say that it’s a small-step semantics on $E cup V$. This is not particularly useful.
• Given a small-step semantics $to$, you can define a corresponding denotational semantics where the denotation of an expression is the set of reduction chains starting from it. This satisfies the formal definition, but it isn’t particularly useful, because it adds a set theoretic overhead to objects which are easier to reason about by looking directly at the syntax.
• Given a denotational semantics $llbracket cdot rrbracket$, you can define a small-step semantics by adding all possible denotations as values in the language. That requires creating values that are not part of the syntax that the programmer can write, which means that some interesting results have to state “for all programs that the programmer can write” rather than “for all programs”. This one is thus not very useful either.
• Given a big-step semantics $Downarrow$, you can define a corresponding denotational semantics where the domain is the set of sets of values: $llbracket e rrbracket = {v mid e Downarrow v}$. If the big-step semantics is deterministic (each expression reduces to a single value), you can define a simpler denotational semantics where the domain is the set of values.
• Conversely, given a denotational semantics $llbracket cdot rrbracket$, you can define a big-step semantics $E Downarrow llbracket cdot rrbracket$. Again this one is a little pointless.

Operationally speaking, small-step semantics corresponds to looking at each operation performed by an interpreter for the language. Big-step semantics only looks at the resulting value. Denotational semantics looks at a mathematical interpretation which may or may not have anything to do with what happens on a computer. Small-step semantics is the most obvious one. It clearly provides useful information about non-terminating programs. More generally, it provides detailed information about the behavior of the program. Denotational semantics transforms syntactic constructs into arbitrary mathematical objects; it can express whatever the scientists wants (you can define the denotation of an expression to be all possible reduction chains from it), but at the cost of adding a level of complexity. It’s used when we do want to abstract away some details such as exactly how the expression is evaluated. Big-step semantics is in the middle: it abstracts away the details of the evaluation but retains the syntactic nature of the result. Usually the concept is used when there is an underlying small-step semantics, as a way to express concisely “$exists (e_1, dots, e_n), e to e_1 to dots e_n text{ and } notexists e’, e_n to e’$” as “$e Downarrow e_n$”. In such constructions, while the concepts are very different (one allows us to talk about individual computation steps and about non-terminating programs, the other doesn’t), the definitions will look very similar, because in this case the rules that define the big-step semantics are basically of the form “if $e_1 to^* e_2$ and … and $e_n to^* v$ and $v$ is a value then $e_1 Downarrow v$”.