39
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ The Wikipedia article on operational semantics looks promising... until one realises that the sum total of information in the "Big-step semantics" section is "This section requires expansion. (February 2011)." $\endgroup$ Jun 5, 2015 at 17:39
  • 1
    $\begingroup$ What is your learning source? What does it contain on the matter? What do you think? Hint: what is the big-step semantics of x = 0; while ( true ) { x = x + 1; }? $\endgroup$
    – Raphael
    Jun 5, 2015 at 21:57
  • $\begingroup$ @Raphael I'm reading Understanding Computation. My thoughts are that small-step approach is to reduce an expression into sub-expressions until it can't be reduced any further and then evaluating that. Big-step seems to be about evaluating things straight away but I don't really any interesting difference between the two methods as they both seem to be about drilling down higher level constructs. $\endgroup$ Jun 6, 2015 at 16:55
  • $\begingroup$ Big-step being about drilling down from higher level constructs by evaluating sub-constructs and small-step by reducing a larger construct, again, into it's sub-constructs. $\endgroup$ Jun 7, 2015 at 9:29

2 Answers 2

47
$\begingroup$

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$”.

$\endgroup$
4
  • $\begingroup$ I'm also learning this, but I have an issue with something you said in your answer that I would like you to clarify. You said "Big-step semantics are kind of in the middle." However, wouldn't small-step actually be the 'middle' model? Consider expressions: A: ((5 + 7) + 3) B: ((5 + 5) + 5) C: ((1 + 2) + 1) D: ((2 + 1) + 1) Denotational would classify even C and D with different values (possibly "C" and "D"), and big-step would classify them both as "4" and both A and B as "15" However, small-step would give you "(12 + 3)" and "(10 + 5)" for A and B, and "(3 + 1)" for C and D. $\endgroup$ Sep 21, 2017 at 18:50
  • $\begingroup$ @TimothySwan Assuming that you want to define the usual arithmetic evaluation, a denotational semantics would not distinguish C and D. A small-step semantics would define a reduction chain like $((2 + 1) + 1) \to 3 + 1 \to 4$. A big-step semantics would be very similar to a denotational semantics: $((2 + 1) + 1) \Downarrow 3$ vs $[\![((2 + 1) + 1)]\!] = 4$. The $4$ in the big-step semantics is the one in the language syntax whereas the $4$ in the denotational semantics is the one from the metatheory, but the distinction is not visible or important in this simple example. $\endgroup$ Sep 21, 2017 at 18:58
  • $\begingroup$ So when you said, 'Denotational semantics assigns a “meaning” to each expression.' you didn't mean uniquely identifying expressions themselves, but some sort of evaluation-independent meaning? Can you provide a simple example that shows clearly the difference between big-step and denotational semantics? Also, please explain the 3 in ((2+1)+1)⇓3 I'm guessing 'denotational' is some end-all value, but in what instance would 'big-step' not necessarily map directly to that? Does the difference have something to do with context, like (a + 1) depending on the environment which contains a ? $\endgroup$ Sep 21, 2017 at 19:22
  • 1
    $\begingroup$ @TimothySwan As long as there are no side effects, no non-determinism and no functions, the denotational semantics of an expression is the value that it evaluates to. Non-determinism is a good way to illustrate the difference between big-step and denotational: the denotation of an expression would be the set of values that it can have: $[\![\mathtt{rand}(1..n)]\!] = \{1,2,\ldots,n\}$, whereas a big-step semantics would have multiple admissible judgements: $\mathtt{rand}(1..n) \Downarrow 1$ and $\mathtt{rand}(1..n) \Downarrow 2$ and ... The 3 was a typo. $\endgroup$ Sep 21, 2017 at 21:24
1
$\begingroup$

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)
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.