Difference Between Small and Big-step Operational Semantics

Question

What's the fundamental difference(s) between small and big-step operational semantics?

I'm having a hard time grasping what it is and the motivation for having the two.

Answer 1

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 \not\rightarrow 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 } \not\exists 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$”.

Answer 2

I felt similar qualms about the difference between small-step and big-step semantics. I think I personally lacked a concrete example, so I will produce one here. I will use Haskell to encode both big-step and small-step semantics in the form of an evaluator.

Consider the simplest possible expression language with just one syntactic construct - If-then-else. Let's define the language.

data Expr = If Expr Expr Expr | E Val deriving Show

type Val = Bool

There is only one possible terminal value in this expression language, which is a Bool.

Now, the simplest to write is big-step operational semantics. Let us call the evaluator evalB (the B indicating the big-step)

evalB :: Expr -> Val
evalB (E val) = val
evalB (If e1 e2 e3) =
  case (evalB e1) of
    True  -> evalB e2
    False -> evalB e3 

Nothing fancy at all. In fact, big-step semantics are the closest possible analogues to interpreters. Note the type Expr -> Val

Now, for the small-step semantics, we call our evaluator evalS.

evalS :: Expr -> Expr
evalS (E val)             = E val
evalS (If (E True) e2 _ ) = evalS e2
evalS (If (E False) _ e3) = evalS e3
evalS (If e1 e2 e3)       = evalS (If (evalS e1) e2 e3)

The above is the small-step semantics. This might seem somewhat unnatural compared to the big-step semantics. My usage of the term unnatural is intentional (Gilles Kahn calls big-step operational semantics as natural semantics, following that small-step might seem unnatural).

The notable difference is the type signature for small-step Expr -> Expr as opposed to Expr -> Val in big-step. As observable, we do not directly reduce the conditional check in the small-step semantics. We evaluate it to another expression, which will recursively continue evaluating it till it reaches a normal form where there are no further evaluation rules (E False or E True). In the process, the interpreter would capture every "small" step of the evaluation. Also, notably the terminal value E val is not reduced further but kept as an expression itself as there are no steps left to reduce (this form is also known as weak-head normal form).

As for the motivation for having these two styles, this example should illustrate the small step is better at capturing each constituent "small" evaluation step of an evaluator. As such this becomes useful for providing meaning to syntactic constructs where intermediate states (or "steps" if you will) are important, such as concurrency operators where the interleaving of states can result in different terminal values. You can try to run the evaluators to check the resultant value from the respective evaluators.

expr = (If (If (E True)  (E True)  (E True)) 
           (If (E True)  (E False) (E True)) 
           (If (E False) (E False) (E True)))

foo = evalB expr

bar = evalS expr

baz = evalB (evalS expr)