Abstract Machines: SECD and CEK
Evaluation
contexts told us where the next redex is by carrying around a context
E — but "search the whole term for the hole, then plug back" is not something
real hardware does. Each step still re-traverses the syntax tree. An abstract machine
removes that waste: it makes evaluation a first-order state-transition system, a tiny
deterministic automaton whose state records everything needed to take the next step in
O(1) — no re-traversal, no re-decomposition. It is the bridge from
mathematical semantics to something you could compile.
The great insight, made precise by Olivier Danvy and colleagues, is that an abstract machine is
a defunctionalized evaluation-context semantics. The context
E — a function "how to finish, given a value" — is reified into a concrete
data structure called a continuation. We will build the cleanest such machine, the
CEK machine, for the call-by-value lambda calculus, run it, and see the continuation
is the context in disguise.
Three registers: Control, Environment, Kontinuation
A CEK state is a triple \langle C,\ E,\ K\rangle:
- C — the control: the lambda term currently being evaluated.
- E — the environment: a finite map from variables to values. Environments
replace substitution — instead of copying a term into another (expensive, and easy to get wrong), we
remember the binding and look it up later.
- K — the kontinuation (spelled with a K so all three initials line up): a data
structure encoding "what to do with the value of C once we have it". This is
the reified evaluation context.
A value is a closure \langle \lambda x.e,\ E\rangle
— a lambda together with the environment that was in force when we met it, so its free variables keep
their meaning later (this is what makes scoping lexical). Continuations have exactly three
shapes:
K \;::=\; \mathsf{mt} \;\mid\; \mathsf{ar}(e,\ E,\ K) \;\mid\; \mathsf{fn}(v,\ K)
\mathsf{mt} is the empty continuation ("we are done — this value is the
answer"). \mathsf{ar}(e,E,K) means "I just finished the function
part of an application; still to do: evaluate the argument e in
environment E, then continue with K".
\mathsf{fn}(v,K) means "I have the function value
v and just finished the argument; apply v, then
continue with K". These correspond one-to-one with the evaluation contexts
E\,e and v\,E from the previous page.
The transition rules
The machine has just five transitions \longmapsto. Three examine the
control; two apply the continuation once a value is in hand.
\langle e_1\,e_2,\ E,\ K\rangle \;\longmapsto\; \langle e_1,\ E,\ \mathsf{ar}(e_2, E, K)\rangle\qquad\text{\small (app: do the function first)}
\langle \lambda x.e,\ E,\ K\rangle \;\longmapsto\; \mathbf{apply}\big(K,\ \langle \lambda x.e,\ E\rangle\big)\qquad\text{\small (lam: build the closure value)}
\langle x,\ E,\ K\rangle \;\longmapsto\; \mathbf{apply}\big(K,\ E(x)\big)\qquad\text{\small (var: look up the value)}
where dispatching on the continuation is:
\mathbf{apply}\big(\mathsf{ar}(e_2, E', K),\ v\big) \;=\; \langle e_2,\ E',\ \mathsf{fn}(v, K)\rangle\qquad\text{\small (now do the argument)}
\mathbf{apply}\big(\mathsf{fn}(\langle \lambda x.e,\ E'\rangle, K),\ v\big) \;=\; \langle e,\ E'[x \mapsto v],\ K\rangle\qquad\text{\small (β: bind and enter the body)}
And the machine halts when a value meets the empty continuation — that is the final answer:
\dfrac{\;}{\ \langle v,\ E,\ \mathsf{mt}\rangle\ \text{ halts, returning the value } v\ }
Notice the β-rule E'[x \mapsto v]: it extends the closure's
captured environment E' (not the caller's!) with the argument. That
one detail is lexical scope, done right.
Watch it run
Trace the identity applied to the identity, (\lambda x.x)\,(\lambda y.y),
starting from \langle C,\ \varnothing,\ \mathsf{mt}\rangle. Reveal one
transition at a time and watch the three registers evolve — the control shrinks toward a value, the
continuation grows then unwinds.
Follow the continuation column. It grows
(\mathsf{mt} \to \mathsf{ar}(\ldots) \to \mathsf{fn}(\ldots)) while we dig into
the application, then shrinks back to \mathsf{mt} as we deliver values
and perform the \beta-step. That growing-and-shrinking stack is the
call stack of a real interpreter — the CEK machine explains where the call stack comes from.
The CEK machine, in code
Every rule above becomes one line. The machine is a function from state to state; the driver iterates it,
printing each state, until a value meets \mathsf{mt}.
type Term =
| { tag: "var"; name: string }
| { tag: "lam"; param: string; body: Term }
| { tag: "app"; fn: Term; arg: Term };
type Value = { tag: "clo"; lam: Term & { tag: "lam" }; env: Env };
type Env = { [name: string]: Value };
type Kont =
| { tag: "mt" }
| { tag: "ar"; arg: Term; env: Env; k: Kont }
| { tag: "fn"; clo: Value; k: Kont };
type State = { c: Term; env: Env; k: Kont } | { done: true; value: Value };
function apply(k: Kont, v: Value): State {
if (k.tag === "mt") return { done: true, value: v }; // halt
if (k.tag === "ar") return { c: k.arg, env: k.env, k: { tag: "fn", clo: v, k: k.k } };
// k.tag === "fn": apply the stored closure to the new value v (β)
const clo = k.clo;
return { c: clo.lam.body, env: { ...clo.env, [clo.lam.param]: v }, k: k.k };
}
function step(s: State): State {
if ("done" in s) return s;
const { c, env, k } = s;
if (c.tag === "app") return { c: c.fn, env, k: { tag: "ar", arg: c.arg, env, k } };
if (c.tag === "lam") return apply(k, { tag: "clo", lam: c, env }); // closure value
return apply(k, env[c.name]); // variable lookup
}
// --- pretty-printing ---
function showT(e: Term): string {
if (e.tag === "var") return e.name;
if (e.tag === "lam") return `λ${e.param}.${showT(e.body)}`;
return `(${showT(e.fn)} ${showT(e.arg)})`;
}
const showV = (v: Value) => `clo(${showT(v.lam)})`;
function showK(k: Kont): string {
if (k.tag === "mt") return "mt";
if (k.tag === "ar") return `ar(${showT(k.arg)}, ${showK(k.k)})`;
return `fn(${showV(k.clo)}, ${showK(k.k)})`;
}
function showEnv(env: Env): string {
const ks = Object.keys(env);
return ks.length ? `{${ks.map((x) => `${x}=${showV(env[x])}`).join(", ")}}` : "∅";
}
function run(c: Term): void {
let s: State = { c, env: {}, k: { tag: "mt" } };
let n = 0;
while (!("done" in s)) {
console.log(`${n++}: C=${showT(s.c)} E=${showEnv(s.env)} K=${showK(s.k)}`);
s = step(s);
}
console.log(`HALT -> ${showV(s.value)}`);
}
const v = (name: string): Term => ({ tag: "var", name });
const lam = (param: string, body: Term): Term => ({ tag: "lam", param, body });
const app = (fn: Term, arg: Term): Term => ({ tag: "app", fn, arg });
// (λx.x) (λy.y)
run(app(lam("x", v("x")), lam("y", v("y"))));
The trace prints four states then HALT -> clo(λy.y): the machine evaluated the
application, bound x to the closure for \lambda y.y, looked
x up, and delivered it to the empty continuation. Every transition was
O(1) — no substitution, no re-scanning the term.
The continuation is a defunctionalized context
- The CEK machine computes exactly the call-by-value semantics: starting from
\langle e,\ \varnothing,\ \mathsf{mt}\rangle, it halts with a value
v iff e evaluates to
v under the evaluation-context (reduction) semantics.
- The continuation K and the evaluation context
E are in bijection: \mathsf{ar}(e,E,K) is the
context K[[\cdot]\,e] and \mathsf{fn}(v,K) is
K[v\,[\cdot]]. Applying the continuation is plugging the hole.
This is why abstract machines are not an ad-hoc trick but a derivable artifact. Start from a
big-step interpreter; make it tail-recursive by adding an explicit continuation function
(CPS transformation); replace those continuation functions with a datatype and a dispatcher
(defunctionalization); and out drops the CEK machine, mechanically. Danvy called this "the
functional correspondence", and it links every machine in this family — CEK, Krivine (for call-by-name),
the SECD — back to a plain recursive evaluator.
In 1964 Peter Landin published "The Mechanical Evaluation of Expressions", introducing the
SECD machine — four registers: Stack (of intermediate values),
Environment, Control (the code to run), and Dump (a
saved S, E, C to restore after a function call returns). The Dump is a call stack of saved
machine states — essentially our continuation, split across registers. The SECD was the execution model
for Landin's language ISWIM ("If you See What I Mean"), the ancestor of every functional
language since; in the same body of work Landin coined the phrase "syntactic sugar" and argued
that a language is best understood as the lambda calculus plus a handful of sugared conveniences. The CEK
machine (Felleisen & Friedman, 1986) is the SECD's leaner descendant: fold the Stack and Dump into a
single continuation and you go from four registers to three.
The classic bug when building one of these machines is to apply a function in the caller's
environment instead of the one the lambda captured. Re-read the β-transition: it extends
E' — the environment stored inside the closure
\langle \lambda x.e, E'\rangle — never the environment that happens to be
active at the call site. Get this wrong and you have implemented dynamic scope by
accident: a free variable in the function body would resolve to whatever binding is live when the
function is called, not where it was written. That is exactly the notorious bug that
made early Lisp dynamically scoped. A closure exists precisely to freeze the definition-site environment;
dropping the environment and keeping only the lambda re-introduces the bug. If your machine has no
environment stored in its values, it is not implementing lexical scope.