THE CESK MACHINE add a Store — now the machine has addresses, and mutation, and abstraction
The CESK machine is the CEK machine plus a fourth component: a Store, a map from addresses to values. The environment now binds variables to addresses, and addresses point into the store. That one indirection buys mutable state (assignment updates the store, not the environment) and, more famously, abstract interpretation: make the store finite and the CESK machine becomes a static analyzer. Van Horn & Might's “Abstracting Abstract Machines” turns any CESK-style interpreter into a program analysis by bounding the store — a single recipe from evaluator to analyzer.
THE TECHNIQUE env binds vars to addresses; store maps addresses to values
A store with addressed cells. The demo allocates two cells and reads one back — the indirection an environment alone cannot express: live demo
HISTORY & CREDIT Felleisen-Friedman 1987 · Van Horn-Might 2010
“State is a hack bolted onto a pure machine.” — the store is a clean fourth component, and bounding it turns the very same machine from an evaluator into a static analyzer. Addresses are the hinge between running a program and analyzing it. cited
1987 · Felleisen & Friedman — CESK: CEK + a store, for mutable state. 2010 · David Van Horn & Matthew Might — “Abstracting Abstract Machines”: bound the store and the CESK machine becomes a program analysis. now · the systematic route from interpreter to static analyzer.
A store of addresses is the one part you can shrink: keep it infinite and the machine runs; make it finite and the same machine analyzes. Evaluator and analyzer, one design. Van Horn-Might 2010
RECOMMEND FOR I-13 store cells, computed
On the canonical compiler, two addressed cells are allocated and one read back (cell1 = cell0 + 1 = 8):
$ i13 run m_cesk.i13 # a store of addressed cells
RUN OK . 10 step(s) . peak stack 2 . call depth 0
cell0 = 7
cell1 = 8
store_cells = 2
Recommend: i13 has no store — and that is the deep reason its arrays are value-semantic (dart 242, 252). Without a store there are no addresses, no aliasing, no mutation-through-a-pointer: a write yields a new value, never an update to a shared cell. So i13 sits on the CEK side (dart 267), never CESK. The upside is exactly Van Horn & Might's insight run in reverse: a machine with no mutable store is already close to its own static analysis — nothing to abstract, because nothing aliases. i13 keeps the store out to keep its single-pass proof honest.