Inference Rules for Mutation
The \(\TirName{DoDeref}\) rule says that dereferencing an address \(\mathord{\texttt{*}}a\) reduces to the value \(v\) stored in the memory cell named by \(a\):
\[
\inferrule[DoDeref]{
[a \mapsto v] \in m
}{
\langle \mathord{\texttt{*}}a , m \rangle \longrightarrow \langle v, m \rangle
}
\]
Note that it would be equivalent to write \(\TirName{DoDeref}\) as follows: \[
\inferrule[DoDeref]{
}{
\langle \mathord{\texttt{*}}a , m \rangle \longrightarrow \langle m(a) , m \rangle
}
\]
The \(\TirName{DoAssignVar}\) rule says that assigning value \(v\) to memory location \(\mathord{\texttt{*}}a\) in memory \(m\) updates memory \(m\) with the cell \([a \mapsto v]\):
\[
\inferrule[DoAssignVar]{
a\in \operatorname{dom}(m)
}{
\langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} v , m \rangle \longrightarrow \langle v, m[a \mapsto v] \rangle
}
\]
The side-condition that the address \(a\) is in the domain of memory \(m\) (i.e., \(a\in \operatorname{dom}(m)\)) says that there is already an allocated memory cell \([a \mapsto v_0]\) in \(m\) so that we are writing \(m[a \mapsto v]\) to mean updating that cell from \(v_0\) to \(v\) in memory \(m\).
We shall see that memory addresses \(a\) are introduced by \(\mathbf{var}\) allocation, so the alternative system that does not check this condition in the \(\TirName{DoAssignVar}\) rule \[
\inferrule[DoAssignVar]{
}{
\langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} v , m \rangle \longrightarrow \langle v, m[a \mapsto v] \rangle
}
\]
is essentially the same (technically, called being bisimilar).
The \(\TirName{DoVarDecl}\) rules describes allocating a new memory cell for a mutable variable: \[
\inferrule[DoVarDecl]{
a\notin \operatorname{dom}(m)
}{
\langle \mathbf{var}\;x\;\texttt{=}\;v_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle {}[ \mathord{\texttt{*}}a /x]e_2 , m[a \mapsto v_1] \rangle
}
\]
We choose a fresh address \(a\), which we state with the side condition that \(a\notin \operatorname{dom}(m)\) and thus the \([a \mapsto v_1]\) is a new cell in the updated memory \(m[a \mapsto v_1]\). The reduced expression \({}[ \mathord{\texttt{*}}a /x]e_2\) is interesting. The scope of variable \(x\) is the continuation expression \(e_2\), so we must eliminate free-variable occurrences of \(x\) in \(e_2\). We do this by substituting the location value \(\mathord{\texttt{*}}a\) corresponding to \(x\) in \(e_2\).
In the following, we repeat the above \(\TirName{Do}\) rules along with the needed \(\TirName{Search}\) for mutable variables:
The \(\TirName{SearchAssign1}\) rule says that if \(e_1\) is not a location value, then we need to reduce it to be able to do the assignment: \[
\inferrule[SearchAssign1]{
e_1 \neq l_1
\and
\langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle
}{
\langle e_1 \mathrel{\texttt{=}} e_2 , m \rangle \longrightarrow \langle e_1' \mathrel{\texttt{=}} e_2 , m' \rangle
}
\]
Note that \(\TirName{SearchAssign1}\) rule is needed if addresses were first-class values (cf. pointers in C and C++). However, we see that it is not actually needed for this variant of JavaScripty where addresses are not first-class. In this case, we can also restrict the syntax of assignment to
\[
\begin{array}{rrrl}
\text{expressions} & e& \mathrel{::=}& x \mathrel{\texttt{=}}e_1
\end{array}
\]
Studying the \(\TirName{DoVarDecl}\) rule, we see that assignment expressions \(x \mathrel{\texttt{=}}e_1\) where \(x\) is in scope would become \(\mathord{\texttt{*}}a \mathrel{\texttt{=}}e_1\) on substitution where either \(\TirName{SearchAssign2}\) or \(\TirName{DoAssignVar}\) would apply.
Indeed, the actual concrete syntax of JavaScript is restricted such that only certain the expression forms like variables can be written on the left-hand–side of assignment.