7. From Evaluator to Abstract Machine

One promise is left standing. The higher-order footnote of chapter 2 observed that its first-order closures are what a higher-order evaluator becomes under defunctionalization, and called running that derivation on its own evaluator a candidate ending for these lectures. This chapter is that ending. The recipe is the functional correspondence of Ager, Biernacki, Danvy, and Midtgaard: make the evaluator's control explicit by rewriting it in continuation-passing style, then trade the continuation functions for first-order data, and an abstract machine appears, not designed but discovered. No step involves a decision; the machine was in the evaluator all along.

The running heart of the evaluator

A machine runs closed programs. Types, neutrals, and quotation, the parts of chapter 2's evaluator that exist to check open terms, play no role at runtime, so the derivation works on the untyped heart. The syntax is chapter 6's Exp, four constructors of nameless lambda calculus with a unit; a value is the unit or a closure, a body paired with the environment it was written in, exactly as in chapter 2:

inductive Value where
  | unit
  | closure (env : List Value) (body : Exp)
deriving Repr, BEq

instance : Inhabited Value := ⟨.unit⟩

The evaluator is chapter 2's eval with everything but running removed: a variable is a lookup, the two introduction forms are already values, and an application evaluates the function, evaluates the argument, and enters the closure.

partial def eval (env : List Value) : Exp -> Option Value
  | .var i => env[i]?
  | .unit => some .unit
  | .lam body => some (.closure env body)
  | .app fn arg => do
    let vf <- eval env fn
    let va <- eval env arg
    let .closure cenv body := vf | none
    eval (va :: cenv) body

The honesty discipline of chapter 1 and chapter 2 carries over unchanged: failure is a value, so an out-of-scope variable returns none, and the definition is partial, because the untyped calculus contains terms with no result at all. The classic one is on the page and, deliberately, never run:

def delta : Exp := .lam (.app (.var 0) (.var 0))

def omega : Exp := .app delta delta

The rest of the computation, made a value

The first transformation makes the evaluator confess what it plans to do between recursive calls. In continuation-passing style every call receives one extra argument, the continuation, a function standing for the rest of the computation. A success returns only by calling it; the two refusals, an unbound variable and a non-function applied, keep chapter 1's shape and hand back none past the plan:

partial def evalK (env : List Value) (e : Exp)
    (k : Value -> Option Value) : Option Value :=
  match e with
  | .var i => do k (<- env[i]?)
  | .unit => k .unit
  | .lam body => k (.closure env body)
  | .app fn arg =>
    evalK env fn fun vf =>
      evalK env arg fun va => do
        let .closure cenv body := vf | none
        evalK (va :: cenv) body k

Read the application case slowly; the whole chapter turns on it. Between evaluating the function and evaluating the argument, the evaluator waits with a definite plan: evaluate the argument next, then apply. Between evaluating the argument and entering the closure it waits with another: apply the function value already in hand. The direct-style evaluator kept those plans implicit in Lean's own call stack; this one writes each plan down as a lambda. Counting the lambdas shows exactly two shapes of plan ever arise, beyond the initial plan of handing the result back.

Defunctionalization

A function type inhabited by only finitely many lambdas can be replaced by an inductive type with one constructor per lambda, together with an apply function giving each constructor its meaning. The move is Reynolds's defunctionalization, and Danvy and Nielsen tour its uses; applied to the continuations here, it yields one constructor per waiting shape, and a continuation built by nesting becomes a list of frames, the machine's stack:

inductive Frame where
  | evalArg (env : List Value) (arg : Exp)
  | applyFn (fn : Value)
deriving Repr

abbrev Stack := List Frame

The payoff of chapter 2's footnote lands here. A closure is to a function value exactly what a frame is to a continuation: its defunctionalized, first-order record. The evaluator had already made that trade for its values; the machine merely finishes the job for its control.

The machine

What remains after both transformations is a first-order transition system. A state either evaluates an expression against an environment under a stack, or gives a value back to the top frame; each transition is one match arm, and a driver runs them to quiescence:

inductive State where
  | going (env : List Value) (e : Exp) (stack : Stack)
  | giving (stack : Stack) (v : Value)
deriving Repr

def step : State -> Option State
  | .going env (.var i) s => do pure (.giving s (<- env[i]?))
  | .going _ .unit s => pure (.giving s .unit)
  | .going env (.lam body) s => pure (.giving s (.closure env body))
  | .going env (.app fn arg) s => pure (.going env fn (.evalArg env arg :: s))
  | .giving (.evalArg env arg :: s) vf => pure (.going env arg (.applyFn vf :: s))
  | .giving (.applyFn (.closure cenv body) :: s) va =>
    pure (.going (va :: cenv) body s)
  | .giving (.applyFn .unit :: _) _ => none
  | .giving [] _ => none

partial def run (s : State) : Option Value :=
  match s with
  | .giving [] v => some v
  | s => do run (<- step s)

def machine (e : Exp) : Option Value := run (.going [] e [])

The correspondence paper identifies the endpoint of this very derivation as Felleisen et al.'s CEK machine, named for its three components: control, environment, continuation. Nothing above was written to match it; the machine fell out. A bounded tracer makes the run visible. In the trace below, []\.0 is a closure over the empty environment, and the seven states walk the identity applied to the unit from program to answer:

def idExp : Exp := .lam (.var 0)

def applyId : Exp := .app idExp .unit

/--
info: eval (\.0 unit)  env []  stack []
eval \.0  env []  stack [arg(unit)]
give []\.0  stack [arg(unit)]
eval unit  env []  stack [apply([]\.0)]
give unit  stack [apply([]\.0)]
eval 0  env [unit]  stack []
give unit  stack []
-/
#guard_msgs in
#eval IO.println <| String.intercalate "\n"
  ((trace 12 (.going [] applyId [])).map showState)

The agreement, checked

The derivation's claim is that nothing observable changed, and the build pins it on closed programs, a twice-application among them: evaluator and machine return the same value, and they refuse the same scope errors.

def twiceExp : Exp :=
  .lam (.lam (.app (.var 1) (.app (.var 1) (.var 0))))

def demo : Exp := .app (.app twiceExp idExp) .unit

#guard eval [] applyId == machine applyId
#guard eval [] demo == machine demo
#guard eval [] (.app idExp idExp) == machine (.app idExp idExp)
#guard (eval [] (.var 0)).isNone && (machine (.var 0)).isNone

The guards state agreement only on the programs they run; both sides are partial functions, and the statement for all programs belongs to the correspondence paper. What this chapter shows is smaller and pointed: the gap between an interpreter and a machine is two mechanical transformations wide.

The same walk exists in a smaller landscape. Hutton's tutorial Programming language semantics: it's easy as 1,2,3 takes the language of integers and addition, nothing else, through the standard semantic styles, and its eighth section derives an abstract machine with exactly this chapter's two moves, continuations and then defunctionalization. A reader who wants the derivation once more, slower and with nothing but numbers in the language, will find it there.

And that closes the arc of these lectures. A parser was assembled by hand, a checker was built on normalization, both were rediscovered inside Lean's own elaborator, the object language moved into its host and its safety became theorems, and at the end the evaluator turned out to have been an abstract machine folded up. No chapter invented its subject; each uncovered structure the previous ones already contained.