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} &E, S_0 \vdash e_1 \to I, S_1 \\ &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—
\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—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