Suggest edit — state

Title

Name

Note

---
title: "state"
type: concept
source: https://www.jemoka.com/posts/kbhstate/
confidence: high
status: active
---

Lambda Calculus with state:
\begin{equation} e \to (x | \lambda x . e | e e | i | \text{new} | {!e} | e := e) \end{equation}
where:
\(new\) allocate a new memory location \(x\) and return pointer (initialize \(x\) to \(0\)) \(!e\) deref a pointer \(e := e\), which is assigning the pointee of the memory location at the first argument to the second argument new \begin{equation} \frac{l \not \in dom(S)}{E,S \vdash \text{new} \to l, S[l=0]} \end{equation}
that is, we need to return to ourselves a new place in memory
dereference \begin{equation} \frac{E, S_0 \vdash e \to l, S_1}{E, S_0 \vdash !e \to S_{1}(l), S_1} \end{equation}
assignment \begin{equation} \frac{\begin{align} &amp;E, S_0 \vdash e_1 \to I, S_1 \\ &amp;E, S_1 \vdash e_2 \to v, S_2 \end{align}}{ E, S_0 \vdash e_1 := e_2 \to v, S_2[I=v]} \end{equation}
store a store is a mapping from memory locations to values&mdash;
\begin{equation} S = [l_1 = 1, l_2 = 42] \end{equation}
where, \(1\) is stored at location \(l_{1}\), and \(42\) is stored at location \(l_2\)
importantly! locations are first class&mdash;we can return pointers
some observations the store is an extra argument in the environment the store is never copied: no evaluation step uses more than one store, and every store is modified at most once the state is unstructured; the whole store is passed to every step of the evaluation even if only a part is used semantics is very costly sequential order of evaluation must be defined (otherwise your state will be inconsistent) there are uncontrolled amount of aliasing of names unstructured states exposes too much since we only look up a few things at a time