Definitional Interpreters

A big-step operational semantics is a wall of inference rules: judgements of the form \rho \vdash e \Downarrow v read "in environment \rho, expression e evaluates to value v". It is precise, but it is paper — you cannot run a wall of rules. A definitional interpreter is the same semantics wearing running shoes: a program in some meta-language (ML, Scheme, TypeScript) whose every clause is one inference rule. Each premise \rho \vdash e_i \Downarrow v_i becomes a recursive call eval(e_i, env); the rule's conclusion becomes what the clause returns. Run the interpreter and you are, quite literally, constructing the derivation tree the semantics only described.

This is the deepest idea in language implementation, and the phrase itself comes from John C. Reynolds' 1972 paper Definitional Interpreters for Higher-Order Programming Languages — the paper that launched a thousand compilers. Its punchline is unsettling and is the theme of this whole page: an interpreter does not fully define a language on its own. It quietly borrows features from the meta-language it is written in — evaluation order, how functions are represented, how control flows — and unless you notice, those borrowed features leak into the language you thought you were defining. Making them explicit, so the interpreter says exactly what it means and nothing more, is the road that leads to continuations, defunctionalisation, and ultimately to real compilers.

From a rule to a clause

Take the big-step rule for a binary addition. On paper it is two premises above a line and a conclusion below:

\dfrac{\rho \vdash e_1 \Downarrow n_1 \qquad \rho \vdash e_2 \Downarrow n_2}{\rho \vdash e_1 + e_2 \;\Downarrow\; n_1 + n_2}

Read it as a recipe and it translates itself. The two premises say "first find the value of the left operand, then the value of the right operand, both in the same environment \rho"; the conclusion says "the whole sum's value is their arithmetic sum". Line by line:

case "add": const n1 = eval(e.left, env); // ρ ⊢ e₁ ⇓ n₁ (left premise) const n2 = eval(e.right, env); // ρ ⊢ e₂ ⇓ n₂ (right premise) return n1 + n2; // ρ ⊢ e₁+e₂ ⇓ n₁+n₂ (conclusion)

The correspondence is exact and mechanical: premises become recursive calls, the conclusion becomes the return, the environment \rho is threaded as a parameter, and side conditions become guards. A whole language semantics — variables, functions, conditionals, let — is a handful of such rules, so a whole definitional interpreter is a handful of such clauses. That is why it is called definitional: reading it is reading the definition of the language.

The interpreter builds the derivation tree

When you evaluate an expression, the recursive calls the interpreter makes trace out exactly the derivation tree that the big-step semantics would draw for the same judgement. Every recursive call is a premise; every return supplies the value that the parent needs. Here is the tree for \varnothing \vdash (\texttt{let } x = 2 \texttt{ in } x + 3) \Downarrow 5. Reveal it in the order the interpreter actually visits the nodes — a call descends, a value comes back:

The shape of the recursion is the shape of the proof. This is the first sense in which the interpreter is faithful to the semantics — but watch the phrase "first the left, then the right". The semantics never said which premise to establish first: a derivation tree is a static object, with no notion of order. The interpreter, being a program, must pick one. That is the first leak, and it is the subject of the next card.

A runnable definitional interpreter

Below is a complete definitional interpreter for a small higher-order language — literals, variables, addition, let, first-class functions (lam) and application (app). Notice that each case is one big-step rule, and that a function value is represented as a closure: the syntactic lam plus the environment in force where it was written. That single design choice is what makes the semantics higher-order. Press Run:

// Abstract syntax of a tiny higher-order language. type Expr = | { kind: "lit"; n: number } | { kind: "var"; name: string } | { kind: "add"; left: Expr; right: Expr } | { kind: "let"; name: string; value: Expr; body: Expr } | { kind: "lam"; param: string; body: Expr } // λparam. body | { kind: "app"; fn: Expr; arg: Expr }; // fn arg // A runtime value is a number or a CLOSURE = code + the environment it captured. type Value = | { tag: "num"; n: number } | { tag: "clo"; param: string; body: Expr; env: Env }; type Env = Record<string, Value>; // eval is the semantics: one clause per big-step rule. function evaluate(e: Expr, env: Env): Value { switch (e.kind) { case "lit": // ρ ⊢ n ⇓ n return { tag: "num", n: e.n }; case "var": // ρ ⊢ x ⇓ ρ(x) return env[e.name]; case "add": { // premises first, then conclude const l = evaluate(e.left, env); const r = evaluate(e.right, env); return { tag: "num", n: (l as any).n + (r as any).n }; } case "let": { // ρ ⊢ e₁ ⇓ v; ρ,x↦v ⊢ body ⇓ w const v = evaluate(e.value, env); return evaluate(e.body, { ...env, [e.name]: v }); } case "lam": // a λ evaluates to a CLOSURE return { tag: "clo", param: e.param, body: e.body, env }; case "app": { // β-reduction, big-step style const fn = evaluate(e.fn, env) as Value & { tag: "clo" }; const arg = evaluate(e.arg, env); // Evaluate the body in the closure's CAPTURED env, extended with the argument. return evaluate(fn.body, { ...fn.env, [fn.param]: arg }); } } } const show = (v: Value) => v.tag === "num" ? String(v.n) : "<closure>"; // let x = 2 in x + 3 ⇓ 5 const p1: Expr = { kind: "let", name: "x", value: { kind: "lit", n: 2 }, body: { kind: "add", left: { kind: "var", name: "x" }, right: { kind: "lit", n: 3 } } }; console.log("let x = 2 in x + 3 =>", show(evaluate(p1, {}))); // let add3 = (λn. n + 3) in add3 (add3 4) ⇓ 10 const add3: Expr = { kind: "lam", param: "n", body: { kind: "add", left: { kind: "var", name: "n" }, right: { kind: "lit", n: 3 } } }; const p2: Expr = { kind: "let", name: "f", value: add3, body: { kind: "app", fn: { kind: "var", name: "f" }, arg: { kind: "app", fn: { kind: "var", name: "f" }, arg: { kind: "lit", n: 4 } } } }; console.log("let f = λn.n+3 in f (f 4) =>", show(evaluate(p2, {})));

Thirty lines, and it runs closures. But notice what the code silently decided that the rules never stated: the two operands of add are evaluated left-to-right (because const l = … runs before const r = …); the argument of app is evaluated before the call (call-by-value, because we evaluate(e.arg, …) eagerly). Swap those lines and you would define a different language — same rules on paper, different behaviour in practice. This is Reynolds' warning in miniature.

Meta-circular interpreters and the leak

A meta-circular interpreter is the extreme case: an interpreter for a language written in that same language — Lisp's eval in Lisp, a Scheme metacircular evaluator in Scheme. It is gloriously compact, because it reuses the host for everything. But that reuse is exactly the problem. If the host is lazy, the defined language looks lazy; if the host is eager, it looks eager. The interpreter has defined nothing about evaluation order — it inherited it. Reynolds catalogued three such leaks, and the whole discipline of principled interpreters is about plugging them:

Evaluation order. Call-by-value vs call-by-name is inherited from the host's own argument-evaluation strategy unless you force the order yourself (e.g. by explicit sequencing or by passing thunks). A "circular" definition of order defines nothing.
How functions are represented. Representing a closure as a host-language function (a "higher-order" interpreter) borrows the host's own closures. Defunctionalisation replaces every such function with a first-order data structure (a tagged record) plus one apply dispatcher — turning the interpreter into something a first-order machine, or a compiler, can implement.
How control flows. A direct-style interpreter borrows the host's call stack and its return mechanism. Rewriting it in continuation-passing style makes "what happens next" an explicit argument — the essential move for compiling non-local control (exceptions, call/cc, tail calls) that no host stack can be relied on to provide.

Reynolds' programme is the arc of this whole module: start with the honest but leaky higher-order interpreter (this page), make functions explicit as closures over environments, make control explicit as continuations, and you have transformed a semantics into a machine.

Reynolds' Definitional Interpreters for Higher-Order Programming Languages was presented at the 1972 ACM National Conference and is one of the most reprinted papers in the field (a "retrospective" edition appeared in 1998, with Reynolds gently noting what the 26-year-old paper got right and what it missed). Its lasting gift is a pair of transformations you can apply to any interpreter, in sequence: convert to continuation-passing style to make control first-order, then defunctionalise to make the continuations first-order data — and what falls out the other end is an abstract machine (a stack machine, a SECD-like beast) that you never designed by hand. Danvy and Nielsen later showed this "interpreter → abstract machine" pipeline is completely mechanical, connecting Reynolds' 1972 insight to the CEK, SECD and Krivine machines. One short paper, the whole back end.

A meta-circular interpreter does not define evaluation order — it inherits it. If your interpreter's behaviour changes when you run it on a different host, you have discovered a leak, not a bug. The fix is to make the order explicit in the interpreter (sequence the calls yourself, or pass thunks/continuations), so the definition stands on its own.
"Higher-order" is not the same as "implementable everywhere". Representing a runtime function as a host closure is elegant but assumes the host has closures. To compile to a first-order target (bytecode, C, a register machine) you must defunctionalise: turn each function into a tagged data structure and write one explicit apply. Skipping that step is why a pretty interpreter can be impossible to turn into a compiler.
Threading the environment is not optional. Every recursive call must pass the environment down, and let/lam must pass an extended one. A closure must capture the environment at definition time, not look it up at call time — mixing those up is the static-vs-dynamic-scope bug you meet on the next page.