⚙️ Abstract Machine Simulator

SECD, CEK, and Krivine machines — three classic evaluation strategies

Overview

Abstract machines bridge the gap between the lambda calculus (a mathematical model of computation) and real interpreters/compilers. Each machine defines a small set of states and transition rules that mechanically reduce lambda terms to values.

This implementation provides three machines side-by-side, all evaluating the same lambda calculus AST, so you can directly compare how call-by-value (SECD, CEK) and call-by-name (Krivine) strategies differ in practice.

The Three Machines

Machine	Strategy	Components	Invented
SECD	Call-by-value (strict)	Stack, Environment, Control, Dump	Landin, 1964
CEK	Call-by-value (strict)	Control, Environment, Kontinuation	Felleisen & Friedman, 1986
Krivine	Call-by-name (lazy)	Term, Environment, Stack of closures	Krivine, 2007 (published)

Shared Lambda Calculus AST

(* All three machines evaluate the same expression type *)
type expr =
  | Var of string           (* variable reference *)
  | Lam of string * expr    (* λx.body — abstraction *)
  | App of expr * expr      (* (f arg) — application *)
  | Int of int              (* integer literal *)
  | Add of expr * expr      (* arithmetic addition *)
  | Mul of expr * expr      (* arithmetic multiplication *)
  | Let of string * expr * expr  (* let x = e1 in e2 *)

SECD Machine

The oldest abstract machine for the lambda calculus. It uses four registers:

Stack — holds intermediate values during evaluation
Environment — maps variable names to values (closures)
Control — list of instructions still to execute
Dump — saved states for returning from function calls

module SECD = struct
  type value =
    | VInt of int
    | VClosure of string * expr * env
  and env = (string * value) list

  type control =
    | CEval of expr
    | CApply

  (* Transition: evaluate application *)
  (* 1. Push CApply, then evaluate arg, then func *)
  (* 2. When CApply fires: save S/E/C to Dump, enter closure body *)
  (* 3. On return: restore from Dump, push result *)
end

CEK Machine

A refinement that replaces the dump with first-class continuations, making the control flow explicit:

module CEK = struct
  type cont =
    | Done
    | ArgK of expr * env * cont    (* evaluate the argument next *)
    | FunK of value * cont         (* apply the function to result *)
    | AddLK of expr * env * cont   (* evaluate right operand of Add *)
    | AddRK of value * cont        (* perform the addition *)
    | ...

  (* State = (Control expr, Environment, Kontinuation) *)
  (* Each step pattern-matches on the triple and produces a new state *)
end

The CEK machine is widely used in PL research because continuations compose cleanly with features like call/cc, exceptions, and delimited control.

Krivine Machine

Unlike SECD and CEK, Krivine implements call-by-name: arguments are not evaluated before being passed. Instead, they are stored as closures (unevaluated expression + environment) on a stack.

module Krivine = struct
  type closure = Clo of expr * env
  and env = (string * closure) list

  (* State = (Term, Environment, Stack of closures) *)
  (* Key rule: App(f, arg) → push Clo(arg, env) onto stack, continue with f *)
  (* When Lam(x, body) meets a stack closure: bind x to the closure, eval body *)
end

This means (λx. 42) (infinite_loop) returns 42 under Krivine but diverges under SECD/CEK, since the argument is never evaluated.

Comparison Examples

(* The implementation runs all three on the same expression *)
let examples = [
  ("identity", App(Lam("x", Var "x"), Int 42), "λx.x applied to 42");
  ("arithmetic", Let("a", Int 3, Let("b", Int 4, Add(Var "a", Var "b"))),
   "let a=3 in let b=4 in a+b");
  ("higher-order", App(App(Lam("f", Lam("x", App(Var "f", Var "x"))),
                          Lam("y", Add(Var "y", Int 1))), Int 5),
   "apply (λf.λx.f x) (λy.y+1) 5");
]

(* Each machine reaches the same result (for terminating, strict programs) *)
(* but through different state transition sequences *)

OCaml Concepts Demonstrated

Modules — each machine is its own module with independent types and eval functions
Mutually recursive types — value and env are co-defined
Variant types for control flow — continuations and control instructions as algebraic data types
Pattern matching — every transition rule is a match arm, making the semantics readable as formal rules
Closures — both in the OCaml implementation and as first-class values in the simulated machines
Substitution vs environments — demonstrates why environment-based evaluation avoids exponential blowup

Running It

# Compile and run
ocamlfind ocamlopt -package str -linkpkg abstract_machine.ml -o abstract_machine
./abstract_machine

# Interactive REPL mode is also available
# Enter lambda calculus expressions to see all three machines evaluate them