Abstract Machines: The CEK, the Krivine Machine, and Closure Conversion

A reduction rule is a statement about terms. An evaluator is a program, and the gap between them is where most of the engineering lives. The calculus says (λx. M) N → M[x := N] and leaves open how to find the redex, how to represent the substitution, and what to do with the result. Every answer to those questions is an abstract machine: an explicit state machine whose states are the configurations a real evaluator passes through, and whose transitions are the steps the calculus describes only abstractly.

The three classic machines differ in which of the three quantities they keep explicit. Control is the term being evaluated. Environment is the mapping from variables to values or closures. Continuation is what remains to be done with the result. A machine that keeps all three as separate registers can be written in a few lines and corresponds directly to a compiler’s calling convention; a machine that keeps only control and environment is smaller but produces its answers in a different form.

Why substitution has to leave the term

The starting point is the cost already noted in the discussion of capture-avoiding substitution: textual substitution copies the argument into every free occurrence, and a term can be substituted many times over. Church’s original presentation used substitution, and the resulting evaluator does work proportional to the size of each substituted body at every step, so a chain of n nested applications can cost O(n²) substitution work.

Landin’s 1964 SECD machine replaced substitution with an environment. The body of a lambda is not copied; it is paired with the environment in effect at the point of abstraction, producing a closure. Applying the closure to an argument extends the environment with a binding from the parameter to the argument and evaluates the body in that extended environment. The term is never rewritten, and the environment grows as a linked structure rather than a copy.

The price is that the result of evaluation is no longer a term. (λx. x) (λy. y) evaluates to a closure holding the term λy. y and an environment, not to the term λy. y. For an interpreter that immediately applies the result, the distinction does not matter. For anything that prints, compares, or serialises the result, it does: a closure has to be reified back into syntax, and the reification can be arbitrarily expensive if the environment is large. This is the same trade that appears in every lazy runtime, where a value in weak head normal form may be a thunk rather than a constructor.

The CEK machine

The CEK machine, named for its three registers of control, environment, and continuation, makes the continuation an explicit stack of frames rather than a property of the host language’s call stack. Its state is a triple ⟨control, environment, continuation⟩, and the transitions are:

⟨x, ρ, κ⟩                  →  ⟨ρ(x), ρ, κ⟩                        variable lookup
⟨M N, ρ, κ⟩                →  ⟨M, ρ, ⟨N, ρ, κ⟩_arg⟩                 evaluate the function
⟨λx. M, ρ, ⟨N, ρ', κ⟩_arg⟩ →  ⟨N, ρ', ⟨x, M, ρ, κ⟩_fun⟩             evaluate the argument
⟨v, ρ', ⟨x, M, ρ, κ⟩_fun⟩  →  ⟨M, ρ[x ↦ v], κ⟩                     apply
⟨v, ρ, □⟩                  →  v                                     halt

The continuation is a stack of frames. The _arg frame records that an argument is pending and remembers the environment in which it must be evaluated; the _fun frame records that a lambda has been found and remembers the body and the environment it closed over, so that the binding can be created once the argument arrives. The two frames together are exactly the two halves of a beta redex, and the transition into the last rule is the beta step, split into its two halves by the fact that the argument is a separate computation.

The environment is a list of bindings, and lookup is a walk. For a term with nesting depth d, a variable costs up to d steps, which is why real implementations use de Bruijn indices and an array: the index is the array offset and lookup is O(1). The machine as written above uses names, which is the presentation that makes the correspondence to the calculus clearest and the implementation slowest.

The continuation stack is where the machine’s memory goes. Each pending argument pushes a frame, so evaluating a left-nested application of depth n uses Θ(n) frames. That is the machine’s version of the call stack, and it is the reason tail calls matter: an application in tail position does not push a frame, because there is nothing to do with the result afterwards. Recognising tail position in the machine is recognising when the continuation is unchanged by a transition.

The Krivine machine and call-by-name

The Krivine machine evaluates under call-by-name, which means the argument is not evaluated before the function is applied. Its state is a triple ⟨term, environment, stack of arguments⟩, and the stack holds unevaluated terms paired with their environments rather than values.

⟨M N, ρ, S⟩              →  ⟨M, ρ, (N, ρ) : S⟩              push the argument unevaluated
⟨λx. M, ρ, (N, ρ') : S⟩  →  ⟨M, ρ[x ↦ (N, ρ')], S⟩          bind the term, not its value
⟨x, ρ, S⟩                →  ⟨M, ρ', S⟩   where ρ(x) = (M, ρ')

The third rule is the one that distinguishes the machine. A variable’s binding is a closure, a term paired with the environment it was created in; looking the variable up replaces the control with that term and the environment with that closure’s environment, leaving the stack untouched. Nothing is evaluated at the lookup. If the term is a lambda and the stack is non-empty, the second rule fires and the top argument is bound; if the stack is empty, the machine has reached a value and stops.

That is the call-by-name application: the argument is only evaluated when, and if, the function actually uses it, and each use re-evaluates it because the environment stores the term and its environment, not the term’s value. A function that ignores its argument never touches the thunk, so (λx. y) Ω terminates in the Krivine machine exactly as normal order predicts.

The Krivine machine has no separate continuation register because the stack is the continuation. It also has no _fun frame: the function position is always evaluated first, and the stack holds only arguments. That makes the machine smaller than the CEK and makes it the natural target for a lazy compiler, since the code for a term is a sequence of “push argument” and “enter closure” instructions.

Weak head normal form is where it stops. A term whose head is a lambda with an empty stack is a value, and the machine halts without reducing the body. That is exactly the behaviour of a lazy runtime returning a closure, and it is why the Krivine machine computes weak head normal forms rather than full normal forms. Reaching a full normal form requires running the machine on the body afterwards, with the environment captured, which is a separate pass.

Call-by-need adds sharing to the Krivine machine: the environment maps variables to mutable cells rather than to terms, and the first lookup fills the cell with the result of evaluating the term. Subsequent lookups read the cell. The machine is then the STG machine used by GHC, modulo details of constructor application and update frames. The transition that matters is the update: after evaluating a thunk, the machine writes the value back into the cell and continues with the original continuation, so the work is not repeated.

Environment representation and its costs

The environment is the part of these machines that most affects performance, and the choices are concrete.

A linked association list maps names to values by a chain of frames, each frame a binder and a value. Extension is O(1) — allocate a frame pointing at the old environment — and lookup is O(d) in the number of binders crossed. Closure creation captures a pointer, so it is O(1). This is the representation that makes the machines as simple as they are written, and it is what a naive interpreter uses.

An array of de Bruijn-indexed slots makes lookup O(1), but extension is not free: a closure that binds one more variable must copy the array or use a persistent structure. Copying is O(d) per binder, which turns closure creation from O(1) into O(d) and rules the plain array out for deep recursion. Persistent arrays (radix tries) give O(log d) extension and lookup with structural sharing, which is the usual compromise in compilers that build closures per call.

A flat closure is the compiler’s answer: the free variables of a lambda are determined statically, and the closure stores exactly those values in a fixed-layout record. Lookup becomes an offset into the record, known at compile time, so there is no search at all. The cost is that the compiler must compute free variables, and that a closure cannot be extended with a binding it did not anticipate. This is closure conversion, and it is the transformation that turns the abstract machine into code a CPU can run.

The numbers differ by more than a constant. A linked list lookup for a variable 100 binders deep is 100 pointer dereferences, each a potential cache miss; at roughly 100 cycles per miss on a contemporary machine that is on the order of ten thousand cycles for one variable access. A flat closure offset is one load from a known address, usually in cache. The reason closure conversion is mandatory in a compiler and optional in an interpreter is that the interpreter’s workloads are small and the compiler’s are not.

Defunctionalising the continuation

The CEK machine’s continuation is a stack of frames, and the machine’s transitions pattern-match on the frame constructor. That is a defunctionalised continuation: the higher-order function “what to do next” has been replaced by a data type whose constructors are the frame kinds, plus a dispatch that interprets them. The transformation is mechanical, and its benefit is that the continuation becomes an ordinary heap object that can be captured, copied, and resumed.

Capturing it is what gives first-class continuations. A frame stack can be copied wholesale, and the copy can be invoked later to resume the computation from that point. The cost is the size of the stack at the moment of capture: a deep recursion captures a deep stack, and resuming it re-runs the pending work.

Defunctionalisation also explains why the machine and the calculus agree. Each transition of the CEK machine corresponds to a step of a reduction relation on configurations, and the machine’s termination corresponds to reaching a value. The correspondence is a simulation theorem, and it is what licenses the claim that an interpreter implements the calculus rather than approximating it. The theorem is not automatic: a machine that evaluates arguments before functions, or that shares where the calculus copies, computes a different relation, and the simulation holds only for the strategy the machine was designed for.

What the machines do not settle

None of the three machines decides how to reach a full normal form, because all of them stop at a value. Full normalisation requires evaluating under binders, which means running the machine on the body of a lambda with the environment captured, and then recursively on the results. For a term with no normal form, that process diverges; for a term with one, the cost is the size of the normal form times the cost of evaluating each node, which can be exponential in the depth because a shared subterm is re-evaluated at every occurrence unless the machine memoises.

None of them decides how to handle effects. A state machine has an order of transitions, so effects can be attached to transitions, but which transitions is a semantic choice: an effect at the point of argument evaluation is call-by-value, an effect at the point of use is call-by-name. The same machine with effects attached differently implements different languages, and the choice is visible to programs that can observe ordering.

And none of them decides the representation of the terms they interpret. A machine over named terms needs an environment keyed by name; a machine over de Bruijn terms needs an environment indexed by integer; a machine over a compiled intermediate representation needs neither, because the variable references have already been resolved to offsets. The three presentations compute the same function and differ in the constant factor by which they do it, and the constant factor is the whole reason compilers exist. The reduction strategy the machines implement is the one analysed in beta reduction and evaluation order, and the terms they evaluate are built from the encodings that give the calculus its data.