Small-step Operational Semantics

In small-step semantics we describe the evaluation of our programs by repeatedly rewriting "reducible expressions" (redexes) until we reach a final state.

Configuration

Our first task in defining the semantics is to figure out how to represent the current state of the program. In general, we need to keep track of where in the program we are and the state of any variables/environment in the program. There are two relevant features of Calc that we should notice: Calc programs can assign to variables and they can print output. Therefore, what should our configuration for Calc contain?

The configuration has three key components:

  1. The program (or program fragment) that we are currently executing.
  2. A map from variable names \(V\) to values \(N\). We'll call this \(\sigma\).
  3. A sequence of outputs from the print statements. We'll call this \(\omega\).

We will write a configuration as \(\langle P, \sigma, \omega \rangle\), where \(P\) is the current program fragment, \(\sigma\) is the variable map (sometimes called a "memory" or a "store"), and \(\omega\) is the current sequence of outputs. If you were implementing the abstract machine, you might represent a configuration as a tuple of an AST, a map, and a list.

We'll say that configurations of this form: \(\langle \texttt{skip}, \sigma, \omega \rangle\) are final. 

def initial_state(prog):
    return (prog, {}, [])

def is_final(state):
    (prog, _, _) = state
    return prog == Skip()

Transition relation

Our next task is to define the transition relation \(\rightarrow \subseteq C \times C\), where \(C\) is the set of configurations.

We'll implement the transition relation with a Python function: 

def step(state):
    (prog, ctx, out) = state
    match prog:









	case _:
	    raise RuntimeError(f'interpreter is stuck on: {state}')

Variables

Let's start by taking a look at the rule that describes the behavior of variables:

\begin{prooftree} \AxiomC{$\sigma[v] = n$} \RightLabel{S-Var} \UnaryInfC{$\langle v, \sigma, \omega \rangle \rightarrow \langle n, \sigma, \omega \rangle$} \end{prooftree}

This rule says that a variable \(v\) evaluates into a number \(n\) when \(\sigma\) contains a mapping \(v \mapsto n\). We give each rule a name so we can refer to it later; this is the small-step variable evaluation rule, so we call it S-Var.

What if there isn't a mapping for \(v\)? We don't have a rule for that case, which means that trying to read from an undefined variable causes execution to become stuck. 

# S-Var
case Var(v) if v in ctx:
    return (Int(ctx[v]), ctx, out)

Binary operators

We can evaluate a binary operator if both of its arguments are numbers:

\begin{prooftree} \AxiomC{$n \oplus n' \equiv n''$} \RightLabel{S-Binop} \UnaryInfC{$\langle n \oplus n', \sigma, \omega \rangle \rightarrow \langle n'', \sigma, \omega \rangle$} \end{prooftree} 
# S-Binop
case Binop(op, Int(n_lhs), Int(n_rhs)):
    match op:
	case "+":
	    n = n_lhs + n_rhs
	case "-":
	    n = n_lhs - n_rhs
	case "*":
	    n = n_lhs * n_rhs
	case "/":
	    n = n_lhs // n_rhs
    return (Int(n), ctx, out)

Print

The rule for print says that if the argument to a print is a number \(n\), then we can add \(n\) to the end of the list of outputs: \[\langle \texttt{print}\ n, \sigma, \omega \rangle \rightarrow \langle \texttt{skip}, \sigma, \omega\ @\ [n] \rangle\quad\text{S-Print}\] We're using \(@\) to mean list concatenation. 

# S-Print
case Print(Int(x)):
    return (Skip(), ctx, out + [x])

Set

An assignment with a numeric parameter updates \(\sigma\): \[ \langle v = n, \sigma, \omega \rangle \rightarrow \langle \texttt{skip}, \sigma[v \mapsto n], \omega \rangle\quad\text{S-Set} \] 

# S-Set
case Set(v, Int(x)):
    ctx1 = ctx.copy()
    ctx1[v] = x
    return (Skip(), ctx1, out)

Skip

A sequence that starts with a skip continues with the right-hand-side of the sequence: \[ \langle \texttt{skip}; s, \sigma, \omega \rangle \rightarrow \langle s, \sigma, \omega \rangle\quad\text{S-Skip} \] 

# S-Skip
case Seq(Skip(), rhs):
    return (rhs, ctx, out)

Progress rules

If you look at the previous rules, you might notice that we don't seem to be able to evaluate nested expressions. That is, we have rules that let us evaluate print 1 or 1 + 2 but not print (1 + 2). We need rules that let us reach inside expressions to evaluate.

These rules are called progress rules, and they describe how execution can reach inside expressions until reaching a redex. The progress rules for Calc are as follows:

\begin{prooftree} \AxiomC{$\langle E_{lhs}, \sigma, \omega \rangle \rightarrow \langle E_{lhs}', \sigma', \omega' \rangle$} \RightLabel{SP-Binop-left} \UnaryInfC{$\langle E_{lhs} \oplus E_{rhs}, \sigma, \omega \rangle \rightarrow \langle E_{lhs}' \oplus E_{rhs}, \sigma', \omega' \rangle$} \end{prooftree} \begin{prooftree} \AxiomC{$\langle E_{rhs}, \sigma, \omega \rangle \rightarrow \langle E_{rhs}', \sigma', \omega' \rangle$} \RightLabel{SP-Binop-right} \UnaryInfC{$\langle N \oplus E_{rhs}, \sigma, \omega \rangle \rightarrow \langle N \oplus E_{rhs}', \sigma', \omega' \rangle$} \end{prooftree} \begin{prooftree} \AxiomC{$\langle E, \sigma, \omega \rangle \rightarrow \langle E', \sigma', \omega' \rangle$} \RightLabel{SP-Print} \UnaryInfC{$\langle \texttt{print}\ E, \sigma, \omega \rangle \rightarrow \langle \texttt{print}\ E', \sigma', \omega' \rangle$} \end{prooftree} \begin{prooftree} \AxiomC{$\langle E, \sigma, \omega \rangle \rightarrow \langle E', \sigma', \omega' \rangle$} \RightLabel{SP-Set} \UnaryInfC{$\langle v = E, \sigma, \omega \rangle \rightarrow \langle v = E', \sigma', \omega' \rangle$} \end{prooftree} \begin{prooftree} \AxiomC{$\langle S, \sigma, \omega \rangle \rightarrow \langle S'', \sigma', \omega' \rangle$} \RightLabel{SP-Seq} \UnaryInfC{$\langle S ; S', \sigma, \omega \rangle \rightarrow \langle S''; S', \sigma', \omega' \rangle$} \end{prooftree}

We'll call these "small-step progress" or SP- rules. They might look complicated, but they are actually quite formulaic.

Consider the SP-Binop-left rule. This rule says that if we have an expression like (2 * 3) + (1 + 2), that has a binary operator at its root, we can take a step of evaluation by applying a rule to the left-hand-side 2 * 3. Applying SP-Binop-left yields 6 + (1 + 3). SP-Binop-right lets us evaluate the right-hand-side, but only if the left-hand-side is a number. Together, these rules enforce a left-to-right evaluation order.

These rules are largely administrative, and larger languages need a lot of them. We'll look at a way to make specifying these rules easier in a few minutes. 

# SP-Binop-right
case Binop(op, Int() as e_lhs, Expr() as e_rhs):
    (e_rhs1, ctx1, out1) = step((e_rhs, ctx, out))
    return (Binop(op, e_lhs, e_rhs1), ctx1, out1)

# SP-Binop-left
case Binop(op, e_lhs, e_rhs):
    (e_lhs1, ctx1, out1) = step((e_lhs, ctx, out))
    return (Binop(op, e_lhs1, e_rhs), ctx1, out1)

# SP-Print
case Print(e):
    (e1, ctx1, out1) = step((e, ctx, out))
    return (Print(e1), ctx1, out1)

# SP-Set
case Set(v, e):
    (e1, ctx1, out1) = step((e, ctx, out))
    return (Set(v, e1), ctx1, out1)

# SP-Program
case Seq(lhs, rhs):
    (lhs1, ctx1, out1) = step((lhs, ctx, out))
    return (Seq(lhs1, rhs), ctx1, out1)

Example evaluation

Now that we have all of our transition rules, we can walk through the evaluation of an example program. Consider the program x = 2; print x * 4;.

\[\langle x = 2; \texttt{print}\ x * 4, \{~\}, [~] \rangle \rightarrow \langle \texttt{skip}; \texttt{print}\ x * 4, \{x \mapsto 2\}, [~] \rangle\]

\[\langle \texttt{skip}; \texttt{print}\ x * 4, \{x \mapsto 2\}, [~] \rangle \rightarrow \langle \texttt{print}\ x * 4, \{x \mapsto 2\}, [~] \rangle\]

\begin{prooftree} \AxiomC{$\{x \mapsto 2\}[x] = 2$} \UnaryInfC{$\langle x, \{x \mapsto 2\}, [~] \rangle \rightarrow \langle 2, \{x \mapsto 2\}, [~] \rangle$} \UnaryInfC{$\langle x * 4, \{x \mapsto 2\}, [~] \rangle \rightarrow \langle 2 * 4, \{x \mapsto 2\}, [~] \rangle$} \UnaryInfC{$\langle \texttt{print}\ x * 4, \{x \mapsto 2\}, [~] \rangle \rightarrow \langle \texttt{print}\ 2 * 4, \{x \mapsto 2\}, [~] \rangle$} \end{prooftree} \begin{prooftree} \AxiomC{$\langle 2 * 4, \{x \mapsto 2\}, [~] \rangle \rightarrow \langle 8, \{x \mapsto 2\}, [~] \rangle$} \UnaryInfC{$\langle \texttt{print}\ 2 * 4, \{x \mapsto 2\}, [~] \rangle \rightarrow \langle \texttt{print}\ 8, \{x \mapsto 2\}, [~] \rangle$} \end{prooftree} \begin{prooftree} \AxiomC{$\langle \texttt{print}\ 8, \{x \mapsto 2\}, [~] \rangle \rightarrow \langle \texttt{skip}, \{x \mapsto 2\}, [8] \rangle$} \end{prooftree}

Note that the last configuration is final, so the program produces the expected output 8.

We can see how the progress rules are used to break down expressions until one of the rewriting rules can apply.

Here's how we would encode and run this example using our Python semantics: 

example = Seq(Set("x", Int(2)), Print(Binop("*", Var("x"), Int(4))))

from calc_syntax import *



def run(prog):
    state = initial_state(prog)
    while not is_final(state):
	state = step(state)
	print(state)

run(example)

(Seq(lhs=Skip(), rhs=Print(expr=Binop(op='*', lhs=Var(name='x'), rhs=Int(val=4)))), {'x': 2}, [])
(Print(expr=Binop(op='*', lhs=Var(name='x'), rhs=Int(val=4))), {'x': 2}, [])
(Print(expr=Binop(op='*', lhs=Int(val=2), rhs=Int(val=4))), {'x': 2}, [])
(Print(expr=Int(val=8)), {'x': 2}, [])
(Skip(), {'x': 2}, [8])

You can download the syntax and small-step semantics implementations.

Contexts

The progress rules are, frankly, exhausting. They make our semantics larger and make evaluating programs cumbersome. Luckily, there is an elegant way to eliminate the need for progress rules entirely!

To understand how, we need to think carefully about what the progress rules are doing. Consider the expression (2 * 3) + (4 - (1 * 5)). The progress rules for binary operators tell us that if the left-hand-side is not a number, then we should rewrite it, so our first reducible expression (or "redex") is 2 * 3. If we rewrite 2 * 3 to 6, yielding 6 + (4 - (1 * 5)), then the progress rules tell us to rewrite the right-hand-sides, so our next redex is 1 * 5. Essentially, the progress rules are identifying redexes, and when there is more than one redex, they tell us in what order the redexes should be evaluated.

We introduce contexts as an alternative way to identify redexes, and show that they make small-step semantics easier to read and write.

A context is simply a term (an AST) with a single hole. For example, □ + 1 is a context (we use □ to mark the hole). We can fill the hole in a context \(C\) with another term \(E\), and we write this as \(C[E]\). We can also take an expression \(E\) and split it into a context \(C\) and an expression \(E'\) such that \(E = C[E']\). One way to think about contexts is that they let us point to a particular sub-expression.

Returning to our example, we can point out the redex by splitting (2 * 3) + (4 - (1 * 5)) into a context □ + (4 - (1 * 5)) and expression 2 * 3. This suggests that we could write a rule like the following, where \(\rightarrow_S\) refers to just the S- rules above.

\begin{prooftree} \AxiomC{$C$ is some context. Will any context do?} \AxiomC{$\langle E, \sigma, \omega \rangle \rightarrow_{S} \langle E', \sigma', \omega' \rangle$} \RightLabel{S-Step?} \BinaryInfC{$\langle C[E], \sigma, \omega \rangle \rightarrow \langle C[E'], \sigma, \omega \rangle$} \end{prooftree}

This rule says that we can take a step of execution if we can split our program into a context \(C\) and a redex \(E\). We take this step by evaluating \(E\) to \(E'\) and putting it back into the context. This describes the evaluation process for expressions pretty well, but there is still a niggling question. Can we choose any context \(C\)? Or do we need to put some restrictions on our choice of \(C\)?

If we apply our proposed rule to (2 * 3) + (4 - (1 * 5)), it allows us to reduce either 2 * 3 or 1 + 5. We want to enforce a left-to-right evaluation order, so this rule is too permissive. We should only be able to reduce 2 * 3.

To regain control over evaluation order, we will only select contexts that match a grammar:

\begin{align} C &::= □ ~|~ n \oplus C ~|~ C \oplus E ~|~ C ; S ~|~ \texttt{print}\ C ~|~ v = C \\ \end{align}

This grammar rules out the problematic out-of-order evaluation of 1 + 5, because (2 * 3) + (4 - □) is not in the set of expression contexts \(C\). We can only build an expression context that places the hole on the right-hand-side of a binary operation if the left-hand-side is a number.

The following (correct!) rule replaces the progress rules with contexts:

\begin{prooftree} \AxiomC{$\langle E, \sigma, \omega \rangle \rightarrow_{S} \langle E', \sigma', \omega' \rangle$} \RightLabel{S-Step} \UnaryInfC{$\langle C[E], \sigma, \omega \rangle \rightarrow \langle C[E'], \sigma, \omega \rangle$} \end{prooftree}

To recap, we can use contexts to simplify the presentation of our semantics. You can always write progress rules instead, but contexts are common in the literature, and we want you to be able to understand them when you encounter them.

Big-step vs small-step

Now that we've seen two styles of operational semantics, we can compare and contrast their properties.

Big-stepSmall-step
Pros
  • Concise
  • Recursive structure models recursive evaluation of expressions
  • Avoids some of the pain around progress rules
  • Great for modeling low level behavior of control flow, concurrency, and errors
Cons
  • Hard to model infinite loops, runtime, and other resource use
  • Amount of detail can be cumbersome
  • Recursive evaluation as in expressions requires progress rules or contexts

We'll lean towards small-step in the rest of the course, particularly when we talk about control flow.

Beyond operational semantics

Operational semantics is just one approach to the problem, and it isn't suitable for all purposes. It's particularly good at describing how programs execute, and it's easy to capture mutable state, nondeterminism, parallelism, and concurrency. It's also quite natural for programmers who are used to thinking about how programs execute one step at a time. Unfortunately, we have to describe the semantics of the entire language at once, which makes it difficult to reason about language features in isolation. It's also unclear how we might use an operational semantics to prove properties of specific programs; we would need some way to reason about the states that the program might end up in and how those states relate to the property we care about.

Other approaches to semantics (denotational, axiomatic) have been developed that offer these properties. We won't spend more time on them in this course, but you might encounter these ideas again in future PL courses.

Further Reading

Last updated: 2023-03-15 Wed 13:47