<p>The store in a CESK machine is the “heap”, where mutable pointer-based data structures live.</p>
<ol>
<li><p>If your language is purely functional, then its operational  semantics don’t need a store. Take it out, and you get the CEK machine.</p>
</li>
<li><p>If your language does not have control operators (such as <code>call/cc</code> or exceptions), then you can get away without the K (the continuation).</p>
</li>
<li><p>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.</p>
</li>
<li><p>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.</p>
</li>
</ol>

CC BY-SA 4.0
2018-07-25T13:45:07.733Z
2024-01-18T22:10:24.983Z
2024-01-18T22:10:24.983Z
Neel Krishnaswami
<p>We know that a CESK machine <a href="http://matt.might.net/articles/cesk-machines/" rel="noreferrer">can be defined as</a>:</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p>Ed Kmett <a href="https://twitter.com/kmett/status/1021095147902316544?cn=ZmxleGlibGVfcmVjc18y&amp;refsrc=email" rel="noreferrer">writes</a> </p>

<blockquote>
  <p>Video from my recent twitch stream on CEK machines is up!</p>
</blockquote>

<p>Matt Might <a href="http://matt.might.net/articles/cek-machines/" rel="noreferrer">writes</a>:</p>

<blockquote>
  <p>Writing CEK-style interpreters (or semantics) in Haskell</p>
</blockquote>

<p>To Matt's credit - he also writes about CESK machines in <a href="http://matt.might.net/articles/cesk-machines/" rel="noreferrer">racket</a> and <a href="http://matt.might.net/articles/oo-cesk/" rel="noreferrer">Java</a>. </p>

<p>But when we read the <a href="https://www.cs.indiana.edu/ftp/techreports/TR202.pdf" rel="noreferrer">original paper</a> ("A Calculus for Assignments in Higher Order Languages") by <a href="https://en.wikipedia.org/wiki/Matthias_Felleisen" rel="noreferrer">Matthias Felleisen</a> and <a href="https://en.wikipedia.org/wiki/Daniel_P._Friedman" rel="noreferrer">Dan Friedman</a> - we find that the original paper describes a CESK machine. </p>

<p>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. </p>

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

CC BY-SA 4.0
2020-01-05T11:33:36.490Z
"The point being the Continuation and the Store are essential" seems to be "The point being the Control and the Store are essential"?
FrankHB
<lambda-calculus>
Is a CEK machine an implementation of a CESK machine?
hawkeye
# Is a CEK machine an implementation of a CESK machine?

(Asked by: username_0 on 2018-07-25)

We know that a CESK machine [can be defined as](http://matt.might.net/articles/cesk-machines/):

> 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](https://twitter.com/kmett/status/1021095147902316544?cn=ZmxleGlibGVfcmVjc18y&refsrc=email)

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

Matt Might [writes](http://matt.might.net/articles/cek-machines/):

> Writing CEK-style interpreters (or semantics) in Haskell

To Matt's credit - he also writes about CESK machines in [racket](http://matt.might.net/articles/cesk-machines/) and [Java](http://matt.might.net/articles/oo-cesk/).

But when we read the [original paper](https://www.cs.indiana.edu/ftp/techreports/TR202.pdf) ("A Calculus for Assignments in Higher Order Languages") by [Matthias Felleisen](https://en.wikipedia.org/wiki/Matthias_Felleisen) and [Dan Friedman](https://en.wikipedia.org/wiki/Daniel_P._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?)

**Tags:** lambda-calculus

> **Comments:**
> **username_1**: "The point being the Continuation and the Store are essential" seems to be "The point being the Control and the Store are essential"?  

---

## 1 answers

### Answer by username_2 on 2018-07-25. Score: 13 | Accepted answer

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 without 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.


---

