CEK Machine

A CEK machine can be created for any programming language so the term is often used vaguely. For example, a CEK machine could be created to interpret the lambda calculus. Its environment maps variables to closures and the continuations are either a halt, a continuation to evaluate an argument (ar), or a continuation to evaluate an application after evaluating a function (ap): == On the untyped lambda calculus ==

In the original paper, the authors describe the CEK machine using small-step operational semantics over the untyped lambda calculus: \begin{align} \langle x, \text{E}, \text{K} \rangle &\mapsto \langle \epsilon, \emptyset, \text{ret}(E[x]) \gg \text{K} \rangle \\ \langle \lambda x . M, \text{E}, \text{K} \rangle &\mapsto \langle \epsilon, \emptyset, \text{ret}((\lambda x . M, \text{E})) \gg \text{K} \rangle \\ \langle M \, N, \text{E}, \text{K} \rangle &\mapsto \langle M, \text{E}, \text{arg}(N, \text{E}) \gg \text{K} \rangle \\ \langle \epsilon, \emptyset, \text{ret}(F) \gg \text{arg}(N, \text{E}) \gg \text{K} \rangle &\mapsto \langle N, \text{E}, \text{app}(F) \gg K \rangle \quad &F = \lambda x . M \\ \langle \epsilon, \emptyset, \text{ret}(V) \gg \text{app}(F) \gg \text{K} \rangle &\mapsto \langle M, \text{E}[x \mapsto V], K \rangle \quad &F = \lambda x . M\\ \end{align} where \gg is a monadic bind on the continuations, \text{E}[x \mapsto V] is an environment extended with a new binding. For example, the term (\lambda x . x + 1) \, 5 is evaluated using the following steps: \begin{align} &\langle (\lambda x . x + 1) \, 5, \text{E}, \text{K} \rangle \\ \mapsto \quad &\langle (\lambda x . x + 1), \text{E}, \text{arg}(5, \text{E}) \gg \text{K} \rangle \\ \mapsto \quad &\langle \epsilon, \emptyset, \text{ret}((\lambda x . x + 1, \text{E})) \gg \text{arg}(5, \text{E}) \gg \text{K} \rangle \\ \mapsto \quad &\langle 5, \text{E}, \text{app}((\lambda x . x + 1, \text{E})) \gg \text{K} \rangle \\ \mapsto \quad &\langle \epsilon, \emptyset, \text{ret}(5) \gg \text{app}((\lambda x . x + 1, \text{E})) \gg \text{K} \rangle \\ \mapsto \quad &\langle x + 1, \text{E}[x \mapsto 5], K \rangle \\ \vdots \\ \mapsto \quad &\langle \epsilon, \emptyset, \text{ret}(6) \gg K \rangle \\ \end{align} where the calculus is extended to numbers and addition (even though both numbers and addition can be encoded entirely in the lambda calculus). == Representation of components ==

Each component of the CEK machine has various representations. The control string is usually a term being evaluated, or sometimes, a line number. For example, a CEK machine evaluating the lambda calculus would use a lambda expression as a control string. The environment is almost always a map from variables to values, or in the case of CESK machines, variables to addresses in the store. The representation of the continuation varies. It often contains another environment as well as a continuation type, for example argument or application. It is sometimes a call stack, where each frame is the rest of the state, i.e. a control statement and an environment. == Related machines ==

There are some other machines closely linked to the CEK machine. CESK machine The CESK machine is another machine closely related to the CEK machine. The environment in a CESK machine maps variables to pointers, on a "store" (heap) hence the name "CESK". It can be used to model mutable state, for example the Λσ calculus described in the original paper. This makes it much more useful for interpreting imperative programming languages, rather than functional ones. == Origins ==

On page 196 of "Control Operators, the SECD Machine, and the \lambda-Calculus", and on page 4 of the technical report with the same name, Matthias Felleisen and Daniel P. Friedman wrote "The [CEK] machine is derived from Reynolds' extended interpreter IV.", referring to John Reynolds's Interpreter III in "Definitional Interpreters for Higher-Order Programming Languages". To wit, here is an implementation of the CEK machine in OCaml, representing lambda terms with de Bruijn indices: type term = IND of int (* de Bruijn index *) | ABS of term | APP of term * term Values are closures, as invented by Peter Landin: type value = CLO of term * value list type cont = C2 of term * value list * cont | C1 of value * cont | C0 let rec continue (c : cont) (v : value) : value = match c, v with C2 (t1, e, k), v0 -> eval t1 e (C1 (v0, k)) | C1 (v0, k), v1 -> apply v0 v1 k | C0, v -> v and eval (t : term) (e : value list) (k : cont) : value = match t with IND n -> continue k (List.nth e n) | ABS t' -> continue k (CLO (t', e)) | APP (t0, t1) -> eval t0 e (C2 (t1, e, k)) and apply (v0 : value) (v1 : value) (k : cont) = let (CLO (t, e)) = v0 in eval t (v1 :: e) k let main (t : term) : value = eval t [] C0 This implementation is in defunctionalized form, with cont and continue as the first-order representation of a continuation. Here is its refunctionalized counterpart: let rec eval (t : term) (e : value list) (k : value -> 'a) : 'a = match t with IND n -> k (List.nth e n) | ABS t' -> k (CLO (t', e)) | APP (t0, t1) -> eval t0 e (fun v0 -> eval t1 e (fun v1 -> apply v0 v1 k)) and apply (v0 : value) (v1 : value) (k : value -> 'a) : 'a = let (CLO (t, e)) = v0 in eval t (v1 :: e) k let main (t : term) : value = eval t [] (fun v -> v) This implementation is in left-to-right continuation-passing style, where the domain of answers is polymorphic, i.e., is implemented with a type variable. This continuation-passing implementation is mapped back to direct style as follows: let rec eval (t : term) (e : value list) : value = match t with IND n -> List.nth e n | ABS t' -> CLO (t', e) | APP (t0, t1) -> let v0 = eval t0 e and v1 = eval t1 e in apply v0 v1 and apply (v0 : value) (v1 : value) : value = let (CLO (t, e)) = v0 in eval t (v1 :: e) let main (t : term) : value = eval t [] This direct-style implementation is also in defunctionalized form, or more precisely in closure-converted form. Here is the result of closure-unconverting it: type value = FUN of (value -> value) let rec eval (t : term) (e : value list) : value = match t with IND n -> List.nth e n | ABS t' -> FUN (fun v -> eval t' (v :: e)) | APP (t0, t1) -> let v0 = eval t0 e and v1 = eval t1 e in apply v0 v1 and apply (v0 : value) (v1 : value) : value = let (FUN f) = v0 in f v1 let main (t : term) : value = eval t [] The resulting implementation is compositional. It is the usual Scott-Tarski definitional self-interpreter where the domain of values is reflexive (Scott) and where syntactic functions are defined as semantic functions and syntactic applications are defined as semantic applications (Tarski). This derivation mimics Danvy's rational deconstruction of Landin's SECD machine. The converse derivation (closure conversion, CPS transformation, and defunctionalization) is documented in John Reynolds's article "Definitional Interpreters for Higher-Order Programming Languages", which is the origin of the CEK machine and was subsequently identified as a blueprint for transforming compositional evaluators into abstract machines as well as vice versa. == Modern times ==

The CEK machine, like the Krivine machine, not only corresponds functionally to a meta-circular evaluator (via a left-to-right call-by-value CPS transformation), it also corresponds syntactically to the \lambda\widehat{\rho} calculus — a calculus that uses explicit substitution — with a left-to-right applicative-order reduction strategy, and likewise for the SECD machine (via a right-to-left call-by-value CPS transformation). == References ==