Notation reference

This book gives a language its meaning with inference rules: compact statements of the form if these facts hold, then this following fact holds. This section explains how to read them and collects the various notations the book uses to formally define semantics. While each notation is introduced and explained when first introduced, this section collects all such notations in one place.

Reading an inference rule

A rule is written with a horizontal line. The statements above the line are its premises, the statement below is its conclusion, and the name on the right identifies the rule:

$\frac{premise _{1} \dots premise _{n}}{conclusion} (Rule-Name)$

Read it downward: when every premise holds, the conclusion holds. The premises are the assumptions the conclusion rests on.

A rule with nothing above the line is an axiom. Its conclusion stands on its own, with nothing to assume. A numeric literal evaluates to itself (writing $⇓$ for evaluates to):

$n ⇓ n (E-Lit)$

When a rule does carry premises, they are the facts that must already hold for it to apply. Addition evaluates each operand, then combines the two results:

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

Derivations

A premise is itself a conclusion: it holds for some reason, and that reason is another rule. Stacking the rules that justify one another produces a derivation — a tree whose leaves are axioms and whose root is the fact you set out to establish. A derivation is a proof that the judgment at its root holds.

Evaluating $(1 + 2) + 4$ builds this tree:

$\frac{\frac{1 ⇓ 1 ( E-Lit ) 2 ⇓ 2 ( E-Lit )}{1 + 2 ⇓ 3} ( E-Add ) 4 ⇓ 4 ( E-Lit )}{( 1 + 2 ) + 4 ⇓ 7} (E-Add)$

Each leaf is an $E-Lit$ axiom; each $E-Add$ step combines two values already derived; the root is the value of the whole expression. Every step is licensed by a rule, so no line of the tree is taken on faith. When the same shape of derivation recurs, it can be recorded as a single derived rule and used directly wherever that shape appears.

Metavariables

The rules use single letters as metavariables — placeholders that range over a kind of object. A subscript or a prime distinguishes several of the same kind ( $e_{1}$ , $e_{2}$ , $v$ , $v^{'}$ ).

Symbol	Ranges over
$e$	expressions
$n$	integer literals
$x$	variable names
$v$	values — the result of evaluation
$ρ$	environments (below)
$σ$	stores (below)
$ℓ$	locations — the identity of a store cell

Evaluating expressions

The central judgment of the semantics is

$ρ ⊢ e ⇓ v$

read in environment $ρ$ , expression $e$ evaluates to value $v$ . The environment $ρ$ records the value of each variable in scope, which is what a variable needs in order to evaluate:

$\frac{ρ ( x ) = v}{ρ ⊢ x ⇓ v} (E-Var)$

Every rule threads the same $ρ$ through its premises, since a subexpression is evaluated in the same scope as the expression containing it:

$\frac{ρ ⊢ e _{1} ⇓ v _{1} ρ ⊢ e _{2} ⇓ v _{2}}{ρ ⊢ e _{1} + e _{2} ⇓ v _{1} + v _{2}} (E-Add)$

An expression with no variables evaluates to the same value under any environment; the arithmetic derivations above drop $ρ$ for that reason and write $e ⇓ v$ .

Threading a store

Once a program can create and overwrite a memory cell, the value of an expression depends on what the cells hold, and evaluating an expression can change them. The store $σ$ — a finite map from locations to values — records those cells, and the judgment carries it, taking one store in and handing one out:

$ρ ⊢ ⟨ e, σ ⟩ ⇓ ⟨ v, σ^{'} ⟩$

read in environment $ρ$ , evaluating $e$ against the store $σ$ yields the value $v$ and leaves the store $σ^{'}$ . The environment goes in but does not come back, since evaluating an expression cannot rebind a name; the store goes in and comes out, since evaluating an expression can change a cell. Threading it left to right through a rule’s premises also fixes the order the subexpressions run in — each premise evaluates against the store the one before it produced:

$\frac{ρ ⊢ ⟨ e _{1} , σ ⟩ ⇓ ⟨ v _{1} , σ _{1} ⟩ ρ ⊢ ⟨ e _{2} , σ _{1} ⟩ ⇓ ⟨ v _{2} , σ _{2} ⟩}{ρ ⊢ ⟨ e _{1} + e _{2} , σ ⟩ ⇓ ⟨ v _{1} + v _{2} , σ _{2} ⟩} (E-Add)$

A form that writes no cell of its own, like $+$ , threads the store through unchanged; the forms that create, read, and write a cell are in the mutation chapter. A program that uses no cell leaves the store the same coming out as going in, and the earlier judgment $ρ ⊢ e ⇓ v$ is that case with the store left implicit. The language reference states the judgment in full, threading the relation database and the outcome of a return alongside the store.