2
$\begingroup$

Wondering if there are any documents, theories, or methodologies for dealing with mutable memory mathematically. Basically a formal algebraic model of how computers manipulate memory. Along the lines of, say I want to model an add operation at a low level, and it writes its output to a register. Then we can model the computer state as a memory, and:

$$add : a \times b \times m \to m'$$

the function $add$ transforms the memory into a different state, holding the final value. Then the second time we call add, the memory is different than it was before. So it's always changing:

$$m \neq m' \neq m'' \neq \dots \neq m^{(n)}$$

Wondering if there are any formalisms out there that deal with this. I would specifically like to see it applied to abstract algebra or category theory. Whereas in abstract algebra typically, everything is immutable and you never worry about "state". I would like to explore the state / mutable memory from a math framework.

$\endgroup$
  • $\begingroup$ Any undergrad textbook on semantics should get you started. (Eike Best's 1996 Book comes to mind.) How complicated all that becomes depends on what language features you want to model. Category (or domain) theory enters the picture when higher order functions are to be modelled. $\endgroup$ – Kai May 24 '18 at 8:35
2
$\begingroup$

See separation logic and theory of arrays in SMT solvers. Both of these provide a principled, mathematically rigorous foundation for reasoning about mutable memory.

$\endgroup$
  • $\begingroup$ Also, Category Theory has a lot of tools (i.e. monads) for dealing with effects (like memory writing) in pure languages. $\endgroup$ – jmite May 9 '18 at 19:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.