3.1. Big-step and Small-step Evaluation🔗

Our semantics for expressions is written in the so-called "big-step" style. Evaluation rules take an expression to a final answer "all in one step":

2 + 2 + 3 * 4 ⇓ 16

But big-step semantics makes it hard to talk about what happens along the way.

Small-step style: alternatively, we can 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

Advantages of the small-step style include:

• Finer-grained "abstract machine", closer to real implementations.

• Extends smoothly to concurrent languages and languages with other sorts of computational effects.

• Separates divergence (nontermination) from stuckness (run-time error).

3.2. A Toy Language🔗

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₂

Notice: each step reduces the leftmost p node that is ready to go — the first rule tells how to rewrite it, the second and third tell where to find it — and constants do not step to anything.

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🔗

The step relation ⟶ is an example of a relation on Tm.

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,

.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))`.