27
$\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$
  • 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$ – David Richerby Jun 5 '15 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 '15 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$ – Simon Morgan Jun 6 '15 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$ – Simon Morgan Jun 7 '15 at 9:29
31
$\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$
  • $\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$ – Timothy Swan Sep 21 '17 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$ – Gilles 'SO- stop being evil' Sep 21 '17 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$ – Timothy Swan Sep 21 '17 at 19:22
  • $\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$ – Gilles 'SO- stop being evil' Sep 21 '17 at 21:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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