Program Semantics

The tree-walking chapter set out the shape of an evaluator: a function that takes an Expr apart and returns its Value, one arm of the walk per rule. Building it is Milestone M1. That evaluator, once written, is one program, and a program cannot be its own definition of the right answer — to say it is correct, we need an account of what evaluating an expression means that stands on its own, ahead of any interpreter. This chapter writes that account for the expressions of Milestone M1. It uses the inference rules the book has been reading since Part I; the notation reference covers how to read a rule and how the rules stack into a derivation. What is new here is the whole rule set at once, and what having it lets us say: which expressions have a value, which have none, and that these rules give no expression more than one.

What the rules specify

Evaluation is the judgment

$e ⇓ v$

read expression $e$ evaluates to value $v$ , defined by the inference rules below. Each rule is a clause of the definition: an expression evaluates to a value exactly when some rule’s conclusion says so and its premises hold. The rules are syntax-directed — the outermost form of $e$ selects which rule can apply — and compositional — a compound expression’s value is built from its subexpressions’ values, named in the premises.

The Milestone M1 fragment has no variables, so the rules here are read in the env-free slice $e ⇓ v$ . Once let and scope arrive in Part III the judgment carries an environment, $ρ ⊢ e ⇓ v$ , and later features add more; the reference states the full judgment — with the store, the relation database, and the $Val / Ret$ outcome — of which every rule below is the value-case, effect-free projection.

The rules for the M1 fragment

Literals

A literal evaluates to the value it denotes. Written for an integer $n$ :

$n ⇓ n (E-Lit)$

The boolean literals true and false, string literals, and the unit value () each evaluate to themselves the same way; $E-Lit$ names all four. The $E-Lit$ rule is an axiom (it has no premise) and it is the base case every derivation ends at.

Arithmetic

Addition evaluates both operands and adds them, provided both are integers:

$\frac{e _{1} ⇓ v _{1} e _{2} ⇓ v _{2} v _{1} , v _{2} \in Z}{e _{1} + e _{2} ⇓ v _{1} + v _{2}} (E-Add)$

Subtraction and multiplication have the identical shape; writing $\oplus$ for either operator:

$\frac{e _{1} ⇓ v _{1} e _{2} ⇓ v _{2} v _{1} , v _{2} \in Z}{e _{1} \oplus e _{2} ⇓ v _{1} \oplus v _{2}} (E-Arith)$

The premise $v_{1}, v_{2} \in Z$ is what confines these operators to integers: when an operand evaluates to a value that is not an integer, no arithmetic rule applies. Division carries one more premise — a nonzero divisor:

$\frac{e _{1} ⇓ v _{1} e _{2} ⇓ v _{2} v _{1} , v _{2} \in Z v _{2} \neq = 0}{e _{1} / e _{2} ⇓ v _{1} \div v _{2}} (E-Div)$

Modulo % has the same rule with the remainder in place of the quotient, and the same $v_{2} \neq = 0$ premise, so a zero divisor matches no rule for either operator. Negation flips the sign of an integer:

$\frac{e ⇓ v v \in Z}{- e ⇓ - v} (E-Neg)$

Comparison and equality

Two families of operator return a boolean, and they differ in the operands they take. The ordering operators ( $<$ , $\leq$ , $>$ , $\geq$ ) take integers, the same restriction the arithmetic rules carry. Writing $\otimes$ for one of them and $\hat{\otimes}$ for the matching order relation on integers:

$\frac{e _{1} ⇓ v _{1} e _{2} ⇓ v _{2} v _{1} , v _{2} \in Z}{e _{1} \otimes e _{2} ⇓ ( v _{1} \otimes ^ v _{2} )} (E-Ord)$

A non-integer operand matches no ordering rule and is stuck.

Equality == and inequality != instead compare structurally: two values are equal when they have the same shape and equal components, so (1, [2]) == (1, [2]) holds. They apply across the M1 value shapes — integers, booleans, strings, unit, tuples, and lists — so their rule needs no premise restricting the operands. Writing $\otimes$ for either operator and $\hat{\otimes}$ for the structural test on values:

$\frac{e _{1} ⇓ v _{1} e _{2} ⇓ v _{2}}{e _{1} \otimes e _{2} ⇓ ( v _{1} \otimes ^ v _{2} )} (E-Eq)$

Later parts extend the structural test to constructor and struct values, and leave it with no result — stuck — on a function or a relation, which have no structural notion of equality. Comparisons do not chain: $a < b < c$ is not a legal expression in Bridger.

Boolean connectives

The and and or operators short-circuit, and the specification denotes that by giving each two rules. A false left operand settles and without the right operand appearing at all:

$\frac{e _{1} ⇓ false}{e _{1} and e _{2} ⇓ false} (E-And-False)$

$\frac{e _{1} ⇓ true e _{2} ⇓ v v \in B}{e _{1} and e _{2} ⇓ v} (E-And-True)$

and or mirrors it — a true left operand settles the result, a false one hands off to the right:

$\frac{e _{1} ⇓ true}{e _{1} or e _{2} ⇓ true} (E-Or-True)$

$\frac{e _{1} ⇓ false e _{2} ⇓ v v \in B}{e _{1} or e _{2} ⇓ v} (E-Or-False)$

$\frac{e ⇓ b b \in B}{not e ⇓ \neg b} (E-Not)$

Because $E-And-False$ has no premise about $e_{2}$ , its conclusion holds whatever $e_{2}$ would do — including when $e_{2}$ has no value at all. Short-circuiting is a consequence of the rules, so it is a fact of the language rather than a habit of one interpreter.

Strings, tuples, and lists

The ++ operator joins two strings, and equally joins two lists; one rule covers both, requiring the operands to be the same one of those two shapes:

$\frac{e _{1} ⇓ v _{1} e _{2} ⇓ v _{2} v _{1} , v _{2} both strings, or both lists}{e _{1} + + e _{2} ⇓ v _{1} + + v _{2}} (E-Concat)$

A tuple evaluates its components left to right and collects the values; its arity is at least two:

$\frac{e _{i} ⇓ v _{i} ( 1 \leq i \leq n )}{( e _{1} , \dots , e _{n} ) ⇓ ( v _{1} , \dots , v _{n} )} (E-Tuple)$

A list evaluates its elements the same way, and the result is the value the reference writes as a cons sequence:

$\frac{e _{i} ⇓ v _{i} ( 1 \leq i \leq n )}{[ e _{1} , \dots , e _{n} ] ⇓ v _{1} :: \dots :: v _{n} :: [ ]} (E-List)$

Neither rule constrains the values its parts produce, so the untyped evaluator builds a tuple or a list from whatever the parts are. Their difference is a typing matter evaluation does not police: a tuple’s positions may each hold a different type, whereas a list’s type [T] fixes one element type for the whole list. The type checker enforces that homogeneity in Part VI, so [1, true] builds a list here and is rejected by the type checker.

A list is also built one element at a time. :: prepends a value to a list, and its rule constrains only the right operand, which must be a list:

$\frac{e _{1} ⇓ v _{1} e _{2} ⇓ v _{2} v _{2} a list}{e _{1} :: e _{2} ⇓ v _{1} :: v _{2}} (E-Cons)$

The value 1 :: [2, 3] is the same list as [1, 2, 3], and the same list the pattern h :: t takes apart in Part VIII: the expression that builds a list and the pattern that inspects one share their notation.

Projecting a tuple

A tuple’s component is read by position with e.i, where the index $i$ is a literal. The projection has a value when the index is in range:

$\frac{e ⇓ ( v _{0} , \dots , v _{n - 1} ) 0 \leq i < n}{e . i ⇓ v _{i}} (E-Proj)$

An index outside $0 \leq i < n$ , or a .i applied to a value that is not a tuple, matches no rule. Lists have no such projection: a list is taken apart by iteration and by patterns in later parts, and the absence of an indexing operator is a deliberate part of the design.

That is the whole M1 fragment. Everything the milestone evaluator computes is one of these rules applied at the root of a derivation whose sub-derivations evaluate the operands. The order in which those operands are evaluated is not observable here, because none of these expressions has an effect; once effects exist, the threaded judgment in the reference fixes the order left to right.

Derivations and stuck expressions

A derivation stacks the rules that justify one another into a tree whose leaves are axioms and whose root is the judgment it establishes. Short-circuiting shows the idea sharply. Take false and (1 / 0 == 0): its whole derivation is one rule over one axiom,

$\frac{false ⇓ false ( E-Lit )}{false and ( 1/0 == 0 ) ⇓ false} (E-And-False)$

The right operand 1 / 0 == 0 does not appear anywhere in the tree, so the expression evaluates to false even though 1 / 0 on its own has no value. A rule is applied only for what its premises demand, and $E-And-False$ demands nothing of $e_{2}$ .

1 / 0 on its own is stuck: no rule concludes a value for it. The only rule for / is $E-Div$ , and its premise $v_{2} \neq = 0$ fails, so there is no derivation of 1 / 0 ⇓ v for any $v$ . The same holds for 1 + true: $E-Add$ is the only rule that could conclude 1 + true ⇓ v, and its premise $v_{1}, v_{2} \in Z$ fails on true, which evaluates to a boolean. A stuck expression is one for which no derivation exists — the absence of a value, rather than a special value standing for failure. The reference gathers the stuck cases of the whole language.

The interpreter of the previous chapters is what makes that absence observable. Where the semantics simply has no tree, eval returns Err(Control::Raise(..)) carrying a RuntimeError, and ? propagates it to the top level — the treatment error handling describes. The two agree: the expressions the rules leave without a derivation are exactly the ones the evaluator reports rather than assigning a value.

Determinism

Reading the rule set as a whole settles one more question: how many values can an expression have? Nothing about inference rules forces the answer to be one — a rule set can license several values for the same expression, and semantics for concurrent or randomized languages do — so it is a property to check rather than assume. Bridger’s rules give at most one. They are syntax-directed, so the form of $e$ picks out the rules that could conclude $e ⇓ v$ . For most forms that is a single rule. Where a form has two — and and or — the rules’ premises are mutually exclusive: $E-And-False$ needs $e_{1} ⇓ false$ and $E-And-True$ needs $e_{1} ⇓ true$ , and $e_{1}$ cannot do both. Since each subexpression in turn has at most one value, each expression built from them does too.

So $e ⇓ v$ is a partial function from expressions to values: every expression has one value or none, and never a choice of two. This is what lets us speak of the value of an expression, and it is why the tree-walker returning a single Value is not making an arbitrary pick among several the rules would allow — the rules allow only one. An expression has no value when it is stuck, and, once the language has recursion, when its evaluation runs forever; a big-step rule set does not distinguish those two cases, a point the next section returns to.

A family of semantic styles

The rules above are one way to give a language meaning: big-step operational semantics, which Kahn named natural semantics, relating an expression directly to its final value. Three other styles answer “what does a program mean” differently, and each is reached for a different purpose.

Small-step (structural operational) semantics, due to Plotkin, gives meaning as a single reduction $e \to e^{'}$ , iterated until no step remains. It exposes the intermediate states a big-step rule passes over, which is what a soundness proof by progress and preservation, and any account of concurrent or interleaved execution, is written against.
Denotational semantics, in the Scott–Strachey tradition, maps each phrase to a mathematical object — a function from inputs to results — assembling the whole from its parts. It is the style for reasoning about when two programs mean the same thing.
Axiomatic semantics, from Floyd and Hoare, gives meaning through what can be proved about a program, in assertions ${P} c {Q}$ . It is the style for verifying that code meets a specification, rather than for computing the value it produces.

This book works in the big-step style throughout. Each rule becomes one arm of the tree-walker, a derivation tree is the evaluator’s call tree, and the judgment $e ⇓ v$ is exactly the type of eval — an expression in, a value out — so the specification and the interpreter have the same shape and can be read against each other. It is also compact enough to be the specification you write for each new feature as it is added, which is how the rest of the book proceeds.

What the style gives up is the intermediate detail. A big-step rule set relates an expression to its final value and describes nothing between, so it cannot tell a computation that runs forever from one that is stuck: each simply lacks a finite derivation. It also fixes no order of steps beyond what the premises thread. Small-step semantics recovers both. Neither matters here — the book has no concurrent execution to describe and treats soundness informally — so big-step gives up nothing this book needs, and keeps the directness of reading as the interpreter it defines.

Concept checks

The expression false and (1 / 0 == 0) evaluates to false, but 1 / 0 on its own is stuck. How do the rules produce both facts?

1 / 0 is stuck because its only rule, E-Div, has the premise $v_{2} \neq = 0$ , which fails, and no other rule concludes a value for a / expression — so there is no derivation of 1 / 0 ⇓ v. false and (1 / 0 == 0) is settled by E-And-False, whose single premise is that the left operand evaluates to false; the rule says nothing about the right operand, so its derivation is just E-And-False over the axiom false ⇓ false, and 1 / 0 never enters the tree. A rule reaches a subexpression only when a premise names it, and short-circuiting is exactly the absence of such a premise in E-And-False.

On 1 + true the rules assign no value at all, rather than a special error value. Why is that the definition, and how does the interpreter make the missing value visible?

The only rule that could conclude 1 + true ⇓ v is E-Add, whose premise $v_{1}, v_{2} \in Z$ fails because true evaluates to a boolean; no other rule applies, so no derivation exists. Being stuck is that absence of a derivation — there is no value, so the semantics invents none. Adding a special “error value” would make it a value like any other, one a later operation could read and carry on from, which is the opposite of “there is no result here.” The interpreter keeps the two apart: it returns Err(Control::Raise(RuntimeError::TypeError { … })) and propagates it with ?, so the absence the rules describe becomes a report at the top level rather than a Value in circulation.

and is defined by two rules, not one. Why does giving a form more than one rule not make evaluation nondeterministic?

Because the two rules cannot both apply to the same expression. E-And-False requires $e_{1} ⇓ false$ and E-And-True requires $e_{1} ⇓ true$ , and since $e_{1}$ has at most one value, at most one of those premises holds. The rules partition the cases rather than offering a choice within one. Determinism needs each expression to have at most one value, and that survives a form having several rules as long as their premises are mutually exclusive — which, across the whole M1 fragment, they are.

A big-step rule set cannot tell a computation that runs forever from one that is stuck; small-step semantics can. Give a setting where that distinction earns its keep, and say why this book can let it go.

The distinction matters most for a soundness proof. Type soundness is often stated as “a well-typed program does not get stuck,” and proved in the small-step style as progress (a well-typed non-value can take a step) and preservation (a step keeps the type). That argument needs the intermediate states — the steps — which big-step discards, and it needs stuckness told apart from looping forever, since a sound language rules out the first while still permitting the second. Reasoning about concurrent or interleaved execution needs the intermediate states for the same reason. This book has no concurrency to describe and treats soundness informally rather than as a step-by-step proof, so it never has to separate the two non-terminating outcomes, and the directness of big-step is worth more to it than the detail it gives up.

The tree-walker already computes values. What does writing the rules down add that reading the interpreter's code does not?

The rules define the right answer independently of the program meant to produce it, so “the evaluator is correct” becomes a claim with content: it agrees with the rules. They also pin down what code leaves implicit. Whether and short-circuits in the language, rather than only in this interpreter, is fixed by E-And-False having no premise about its right operand; whether an expression may have two values is answered by the rules being a partial function; which expressions are errors is answered by which have no derivation. And because each rule maps to one arm, the rule set is the recipe for extending the evaluator: to add a feature, write its rules, then add the arms that mirror them.

A Practical Introduction to Programming Language Design