Formal Model of Immutability Wondering if there is a formal model / algebra / etc. of immutability. This comes up in functional programming with persistent data structures, but I haven't seen any pure math related to it.
For example, given an operation $\circ$ and two sets $A$ and $B$, then $A \circ B = C$. But if you wanted to "undo" $C$, there might not be enough information in $C$ to get back to $A$ unless $C$ preserved the structure of $A$ and $B$. It is preserved in persistent data structures, which got me wondering if there is a formal model for it.
 A: In mathematics, objects are immutable by definition in any given context. However, if you define $\;x=3\;$ in one context, then you can define $\;x=1\;$ in some other context, but it is immutable in any given context. Of course, variables may have more than one value, or else none. This is not mutability though. The concept of indexed object is perhaps what you mean. That is, for example, $\;a_0=1,\; a_n=2a_{n-1}\;$ is an indexed object which changes with the index. Of course, $\;a_n=1\;$ for all $\;n\;$ is a constant object which does not change with the index.
As for your idea of "undo", all that involves is operations having an inverse. Some operations have inverses and others don't. For example, $\;A+B=C\;$ can be "undone" by $\;A=C-B.\;$ This is an important property of addition as a group operation, but in general, you can't "undo" operations.
When you switch from the mathematical realm to the realm of reality, then things are very different. This is only natural. Different rules apply to different realms. As Heraclitus stated "everything changes" (in Greek). Constrast this with Plato's  immutable, ideal Forms. These are perrenial philosophical issues.
However, even the Greeks were able to "model" the movment of some heavenly bodies. Thus, in mathematics there is the study of "dynamical systems" which studies the properties of models of changing systems. Thus, in this sense, you can develop models of mutable and immutable objects, but in the context of programming langues. Perhaps this is what you mean.
