Inference Rules and Judgements

In the last two lessons we built expression trees and gave them meaning with a semantic function \llbracket \cdot \rrbracket. That worked because arithmetic is simple. But most interesting facts about programs are not "what number is this?" — they are relations: "this expression evaluates to that value", "this term has that type", "this state steps to that one". The universal language for defining such relations, used on essentially every page of programming-language theory, is the inference rule. Master its notation and you can read the semantics of any language — because they are all written this way.

The unit of currency is the judgement: an assertion that might hold, written in some fixed form. e \Downarrow v ("e evaluates to the value v") is a judgement. So is \vdash e : \tau ("e has type \tau") and n \text{ even}. A judgement is just a claim — the rules are what tell us which claims are actually derivable.

The shape of a rule: premises over conclusion

An inference rule is written as a horizontal bar. Above the bar go the premises — the judgements that must already hold. Below it goes the single conclusion — the judgement we may then assert. Read the bar as the word "therefore", or "if all of the above, then the below":

\dfrac{J_1 \quad J_2 \quad \cdots \quad J_k}{J}\;\text{(Name)}

A rule with no premises (k = 0) has nothing above the bar; it asserts its conclusion unconditionally. Such a rule is an axiom. A rule with premises is a genuine inference step. Each rule is really a schema: it contains metavariables (like e_1, n, v) standing for arbitrary terms, and you get a concrete instance by substituting actual terms for them — so the two-line schema below stands for infinitely many concrete additions at once.

Let us define the even numbers this way — the classic first example. Two rules, one an axiom:

\dfrac{\;}{0 \text{ even}}\;\text{(E-Zero)} \qquad\qquad \dfrac{n \text{ even}}{n+2 \text{ even}}\;\text{(E-Step)}

(E-Zero) is an axiom: 0 is even, no questions asked. (E-Step) says: if n is even, then so is n+2. Together they pin down exactly the even numbers — and, importantly, only the even numbers, as we make precise below.

A rule set for evaluation

Now the real target: an operational semantics for our arithmetic language, given as a big-step evaluation relation e \Downarrow v. Three rules, one per syntactic form:

\dfrac{\;}{n \Downarrow n}\;\text{(E-Num)} \qquad \dfrac{e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2}{e_1 + e_2 \Downarrow v_1 + v_2}\;\text{(E-Add)} \qquad \dfrac{e_1 \Downarrow v_1 \quad e_2 \Downarrow v_2}{e_1 \times e_2 \Downarrow v_1 \times v_2}\;\text{(E-Mul)}

Watch the object/metalanguage border once more. In (E-Add), the + in the conclusion's subject e_1 + e_2 is object syntax — a tree node. The + in v_1 + v_2 is metalanguage integer addition — it is what actually computes the result. The rule says: "to evaluate a syntactic sum, evaluate both subexpressions to values, then really add those values." Each rule is a schema over the metavariables e_1, e_2, v_1, v_2, n.

Derivations are trees

A single rule rarely finishes the job — its premises are themselves judgements needing justification. So we stack rules: the conclusion of one rule becomes a premise of the next, and we keep going until every branch terminates in an axiom. The result is a derivation tree (or proof tree). Here is the derivation of (1+2)\times 2 \Downarrow 6, revealed from the leaves down to the root:

Written in the traditional stacked notation, the same tree is:

\dfrac{ \dfrac{ \dfrac{\;}{1 \Downarrow 1}\text{(E-Num)} \quad \dfrac{\;}{2 \Downarrow 2}\text{(E-Num)} }{1 + 2 \Downarrow 3}\text{(E-Add)} \qquad \dfrac{\;}{2 \Downarrow 2}\text{(E-Num)} }{(1+2)\times 2 \Downarrow 6}\text{(E-Mul)}

Two ways to read it. Top-down (root last) it is a computation: the leaves supply values, and each bar combines them, until the root delivers 6. Bottom-up (root first) it is a proof search: to justify the root we must find a rule whose conclusion matches it, then recursively justify that rule's premises. The very shape of the tree mirrors the shape of the syntax tree of (1+2)\times 2 — which is exactly why the next lesson can do induction over derivations.

The least relation closed under the rules

A rule set does not just list some true judgements — it defines a whole relation, and it does so with a precise, non-negotiable meaning. The relation defined by a set of rules is the smallest set of judgements that is closed under all the rules: it contains every axiom, it contains the conclusion of any rule whose premises it already contains, and it contains nothing else.

The word least is the whole game. It is what lets us say the even-number rules define only the evens: 3 \text{ even} is not derivable, so — the relation being the smallest closed set — it is simply not in the relation. Without "least", a set containing 3 \text{ even} is also closed under the rules, and the definition would be hopelessly loose. "Least closed set" and "has a finite derivation" are two views of the same thing, and their agreement is precisely what powers rule induction — the proof technique of the next lesson.

Rules, run as code

A big-step rule set transcribes almost mechanically into a recursive evaluator: one clause per rule, the recursive calls being the premises. But we can do something more faithful — build the derivation tree itself as data, so you can see the structure the rules produce, not just the final number. Press Run:

type Exp = | { tag: "num"; n: number } | { tag: "add"; l: Exp; r: Exp } | { tag: "mul"; l: Exp; r: Exp }; const num = (n: number): Exp => ({ tag: "num", n }); const add = (l: Exp, r: Exp): Exp => ({ tag: "add", l, r }); const mul = (l: Exp, r: Exp): Exp => ({ tag: "mul", l, r }); // A node of the DERIVATION tree: the rule used, the judgement proved, and the sub-derivations. type Deriv = { rule: string; judgement: string; premises: Deriv[]; value: number }; // Build the derivation for e ⇓ v by following the rules (E-Num, E-Add, E-Mul). function derive(e: Exp): Deriv { switch (e.tag) { case "num": return { rule: "E-Num", judgement: `${e.n} ⇓ ${e.n}`, premises: [], value: e.n }; case "add": { const d1 = derive(e.l), d2 = derive(e.r); const v = d1.value + d2.value; // metalanguage + return { rule: "E-Add", judgement: `(${show(e)}) ⇓ ${v}`, premises: [d1, d2], value: v }; } case "mul": { const d1 = derive(e.l), d2 = derive(e.r); const v = d1.value * d2.value; // metalanguage * return { rule: "E-Mul", judgement: `(${show(e)}) ⇓ ${v}`, premises: [d1, d2], value: v }; } } } function show(e: Exp): string { switch (e.tag) { case "num": return String(e.n); case "add": return `${show(e.l)}+${show(e.r)}`; case "mul": return `${show(e.l)}*${show(e.r)}`; } } // Pretty-print the derivation tree, indented — leaves are axioms. function print(d: Deriv, indent = ""): void { console.log(`${indent}${d.judgement} [${d.rule}]`); for (const p of d.premises) print(p, indent + " "); } // Derive (1 + 2) * 2 ⇓ 6. print(derive(mul(add(num(1), num(2)), num(2))));

The printed tree is the same one the diagram animates: an E-Mul at the root, an E-Add and an E-Num as its premises, E-Num axioms at every leaf. Because the recursion bottoms out at numerals, the derivation is always finite — every arithmetic expression has exactly one derivation, a fact we will prove properly next lesson.

The horizontal-bar layout is Gerhard Gentzen's, from his 1934–35 doctoral work inventing natural deduction and the sequent calculus. Gentzen wanted a formal system that mirrored how mathematicians actually reason — introducing and eliminating connectives step by step — and the premises-over-conclusion bar was his notation for a single such step. It was pure logic, decades before programming languages existed. The bridge to computing came through the Curry–Howard correspondence: proofs are programs, and a typing derivation \vdash e : \tau is literally a Gentzen-style proof that the type \tau is inhabited. When Gordon Plotkin wrote his enormously influential 1981 notes "A Structural Approach to Operational Semantics" (SOS), he took Gentzen's rules and used them to define how programs run — and the entire modern style of "define your language as a set of inference rules" was born. Every \Downarrow and \to you meet in this course is Gentzen's bar, wearing a programmer's hat.

The classic error is to forget the word least and treat a rule set as "these judgements are true, and I'm not told about the rest." That reading breaks the moment you want to prove a negative — that 3 \text{ even} does not hold, or that evaluation is deterministic. Those facts are true only because the relation is the least closed set: a judgement is out unless a finite derivation forces it in. Drop "least" and you can no longer conclude anything is absent, and rule induction (next lesson) collapses.

A second trap: confusing a rule with a derivation. A rule is a reusable schema with metavariables — one bar. A derivation is a finished tree of concrete rule instances, with axioms at every leaf. "(1+2)\times 2 \Downarrow 6 is derivable" is a statement about the whole tree existing; it is not a single rule. And a would-be derivation whose leaves are not all axioms — one that still has an unjustified premise dangling at the top — proves nothing at all. Every leaf must be an axiom, or the tree is unfinished.