Is a CEK machine an implementation of a CESK machine?

Question

We know that a CESK machine can be defined as:

a state-machine in which each state has four components: a (C)ontrol component, an (E)nvironment, a (S)tore and a (K)ontinuation. One might imagine these respectively as the instruction pointer, the local variables, the heap and the stack.

Ed Kmett writes

Video from my recent twitch stream on CEK machines is up!

Matt Might writes:

Writing CEK-style interpreters (or semantics) in Haskell

To Matt's credit - he also writes about CESK machines in racket and Java.

But when we read the original paper ("A Calculus for Assignments in Higher Order Languages") by Matthias Felleisen and Dan Friedman - we find that the original paper describes a CESK machine.

The paper also describes a CS machine - but not a CEK machine. The point being the Continuation and the Store are essential, but the Environment and the Continuation are negotiable.

My question is: Is a CEK machine an implementation of a CESK machine? (ie isn't the Store Essential?)

Answer 1

The store in a CESK machine is the "heap", where mutable pointer-based data structures live.

1. If your language is purely functional, then its operational semantics don't need a store. Take it out, and you get the CEK machine.

2. If your language does not have control operators (such as call/cc or exceptions), then you can get away with the K (the continuation).

3. If you don't want to model environments and closures explicitly -- that is, you don't mind a substitution-based semantics -- then you don't need the E (the environment). Calculi for classical logic (which have control operators but no state) often end up looking like CK machines.

4. If you have a purely functional language without control effects, then you can use the program itself as the abstract machine state, and the reduction rules will be the small-step operational semantics for that language.