3.1. Big-step and Small-step Evaluation🔗

The evaluators we saw for Slang were formulated in a "big-step" style: they specify how a given expression can be evaluated to its final value "all in one big step":

2 + 2 + 3 * 4 ⇓ 16

This style is simple and natural for many purposes — indeed, Gilles Kahn, who popularized it, called it natural semantics. But there are some things it does not do well. In particular, it does not give us a convenient way of talking about concurrent programming languages, where the semantics of a program — the essence of how it behaves — includes not just which input states get mapped to which output states, but also the intermediate states that it passes through along the way; this is crucial, since these states can also be observed by concurrently executing code.

Another shortcoming of the big-step style is more technical but equally critical in many situations. Suppose we want to define a variant of our expression language where a value could be either a number or a list of numbers. In the syntax of this extended language, it will be possible to write strange expressions like 2 + nil, and our semantics for arithmetic expressions will then need to say something about how such expressions behave. One possibility is to maintain the convention that every arithmetic expression evaluates to some number by choosing some way of viewing a list as a number — e.g., by specifying that a list should be interpreted as 0 when it occurs in a context expecting a number. But this would be a bit of a hack.

A much more natural approach is simply to say that the behavior of the expression 2 + nil is undefined — i.e., it doesn't evaluate to any result at all. And we can easily do this: we just have to formulate aeval and beval as inductive propositions rather than functions, so that we can make them partial functions instead of total ones.

Now, however, we encounter a subtlety that will become important once we move to a full programming language with looping. There, a program might fail to produce a result for two quite different reasons: either because the execution gets into an infinite loop or because, at some point, the program tries to do an operation that makes no sense, such as adding a number to a list, so that none of the evaluation rules can be applied.

These two outcomes — nontermination vs. getting stuck in an erroneous configuration — should not be confused. In particular, we want to allow the first (because permitting the possibility of infinite loops is the price we pay for the convenience of programming with general looping constructs) but prevent the second (which is just wrong), for example by adding some form of typechecking to the language. Indeed, this will be a major topic of the next chapter, on types. As a first step, we need a way of presenting the semantics that allows us to distinguish nontermination from erroneous "stuck states."

So, for lots of reasons, we'd like to have a finer-grained way of defining and reasoning about program behaviors. This is the topic of the present chapter. Our goal is to replace the "big-step" Eval relation with a "small-step" relation that specifies, for a given program, how its atomic steps of computation are performed. In the small-step style, we show how to "reduce" an expression to a simpler form by performing a single step of computation:

2 + 2 + 3 * 4
⟶ 2 + 2 + 12
⟶ 4 + 12
⟶ 16

3.2. A Toy Language🔗

To save space, we start with an incredibly simple language of just constants and addition. (We use single-letter constructors c and p — for Constant and Plus — for brevity.) The same techniques scale up to richer languages.

A standard big-step evaluator, as a function.

Here is the same evaluator, written in exactly the same style, but formulated as an inductively defined relation. We use the notation t ⇓ n for "t evaluates to n."

The notation command below is how that is declared: it introduces ⇓ as infix syntax for the Eval relation defined with it, with a precedence saying how tightly it binds. This is the lightweight way to name a relation; later chapters, where a whole object language needs a grammar rather than a single operator, reach for declare_syntax_cat instead.

                        -------                (const)
                        c n ⇓ n

                        t₁ ⇓ n₁
                        t₂ ⇓ n₂
                    -----------------          (plus)
                    p t₁ t₂ ⇓ n₁ + n₂

Now, here is the corresponding small-step relation, written t ⟶ t':

                -------------------------------      (plus)
                p (c n₁) (c n₂) ⟶ c (n₁ + n₂)

                         t₁ ⟶ t₁'
                    --------------------             (plusLeft)
                    p t₁ t₂ ⟶ p t₁' t₂

                         t₂ ⟶ t₂'
                 ----------------------------        (plusRight)
                 p (c n₁) t₂ ⟶ p (c n₁) t₂'

Things to notice:

• We are defining a single reduction step, in which just one p node is replaced by its value.

• Each step finds the leftmost p node that is ready to go (both of its operands are constants) and rewrites it in place. The first rule tells how to rewrite this p node itself; the other two rules tell how to find it.

• A term that is just a constant cannot take a step.

Let's pause and check a couple of examples of reasoning with the step relation.

If t₁ steps to t₁', then p t₁ t₂ steps to p t₁' t₂.

.p
  (.p
    (.c 1)
    (.c 2))
  (.p
    (.c 1)
    (.c 2))

.c 1

3.3. Relations🔗

We will be working with several different single-step relations, so it is helpful to generalize a bit and state a few definitions and theorems about relations in general. (The optional chapter Rel in Logical Foundations develops some of these ideas in a bit more detail; reviewing that chapter may be useful if the treatment here feels too terse.)

A binary relation on a type X is a family of propositions parameterized by two elements of X — i.e., a proposition about pairs of elements of X.

Our main examples of such relations in this chapter will be the single-step reduction relation, ⟶, and its multi-step variant, ⟶*, defined below, but there are many other examples — e.g., the "equals," "less than," "less than or equal to," and "is the square of" relations on numbers, and the "prefix of" relation on lists and strings.

One simple property a relation may have is being deterministic: like Slang's big-step evaluation, each element is related to at most one other.

Theorem: For each t, there is at most one t' such that t steps to t'. We prove it by induction on the derivation of the first step.

Proof sketch: We show that if x steps to both y₁ and y₂, then y₁ and y₂ are equal, by induction on a derivation of x ⟶ y₁. There are several cases, depending on the last rule used in this derivation and the last rule in the given derivation of x ⟶ y₂.

• If both are plus, the result is immediate.

• The cases when both derivations end with plusLeft or plusRight follow by the induction hypothesis.

• It cannot happen that one is plus and the other is plusLeft/plusRight, since this would imply that x has the form p t₁ t₂ where both t₁ and t₂ are constants (by plus) and one of t₁ or t₂ has the form p _.

• Similarly, it cannot happen that one is plusLeft and the other is plusRight, since this would imply that x has the form p t₁ t₂ where t₁ has both the form p t₁₁ t₁₂ and the form c n.

Formally,

                ------------------------------      (plus)
                p (c n₁) (c n₂) ⟶ c (n₁ + n₂)

                         t₁ ⟶ t₁'
                    -------------------             (plusLeft)
                    p t₁ t₂ ⟶ p t₁' t₂

                         IsValue v₁
                         t₂ ⟶ t₂'
                    -------------------             (plusRight)
                    p v₁ t₂ ⟶ p v₁ t₂'

.p (.p (.c 1) (.c 2)) (.c 3)

Three:  `.p (.p (.c 1) (.c 2)) (.c 3)` itself is a value;
`.p (.c 3) (.c 3)` is a value; `.c 6` is a value.

.p (.p (.c 1) (.c 2)) (.p (.c 3) (.c 4))

Two: `.p (.c 3) (.p (.c 3) (.c 4))` via `plusLeft` and
`.p (.p (.c 1) (.c 2)) (.c 7)` via `plusRight`.

.p (.c 1) (.c 3)

Three: `plus` yields `.c 4`; `plusLeft` with `funny` yields
`.p (.p (.c 1) (.c 0)) (.c 3)`; `plusRight` with `funny` yields
`.p (.c 1) (.p (.c 3) (.c 0))`.