Meeting 24 - Mutable State

Dakota Bryan

Tuesday, November 19, 2024

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferrule}[3][]{ \let\and\qquad \begin{array}{@{}l@{}} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

Meeting 24 - Mutable State

Announcements

  • Anish leading Thursday’s class which will be a review session

    • Fill out this piazza poll to vote on which questions to go over

Today

  • Triage your questions

  • Mutable State

    • Let’s add updatable variables to our language.

    • This will require keeping track of memory and thus, a new judgment form.

    • We will implement this with encapsulated effects.

Mutable Variables Syntax

  • What do we need to add to our syntax to include mutable variables?

Our New Syntax

\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& n \mid x \mid\mathbf{var}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 \mid e_1 \mathrel{\texttt{=}}e_2 \\ & & & \mid\mathord{\texttt{*}}e_1 \mid a \\ \text{variables} & x \\[1ex] \text{values} & v& \mathrel{::=}& n \\ \text{location values} & l& \mathrel{::=}& \mathord{\texttt{*}}a \\ \text{addresses} & a \end{array} \]

Memories

  • Why do we need memory to handle mutable variables?
  • How can we represent memory in our semantics?

New Judgment Form

\[ \langle e, m \rangle \longrightarrow \langle e', m' \rangle \]

\[ \begin{array}{rrrl} \text{states} & \sigma& \mathrel{::=}& \langle e, m \rangle \end{array} \]

Some Inference Rules

\[ \inferrule[DoDeref]{ [a \mapsto v] \in m }{ \langle \mathord{\texttt{*}}a , m \rangle \longrightarrow \langle v, m \rangle } \]

\[ \inferrule[DoAssignVar]{ ??? }{ \langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} v , m \rangle \longrightarrow \langle ??? , ??? \rangle } \]

Variable Decleration

\[ \inferrule[DoVarDecl]{ ??? }{ \langle \mathbf{var}\;x\;\texttt{=}\;v_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle ??? , ??? \rangle } \]

  • How do we represent that \(a\) must be a new address?

  • How do we update the memory?

  • Considering the \(\TirName{DoDeref}\) rule, how should we modify \(e_2\)?

Updates

  • Now, we see that the user has no reason to write \(\mathord{\texttt{*}}a\) on the left side of an assignment. We are abstracting the memory manipulation away, and can update our syntax and semantics to reflect that.

\[ \inferrule[DoAssignVar]{ }{ \langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} v , m \rangle \longrightarrow \langle v, m[a \mapsto v] \rangle } \]

\[ \begin{array}{rrrl} \text{expressions} & e& \mathrel{::=}& x \mathrel{\texttt{=}}e_1 \end{array} \]

Inference Rules - Do Rules

\(\fbox{$ \langle e, m \rangle \longrightarrow \langle e', m' \rangle $}\)

\(\inferrule[DoDeref]{ }{ \langle \mathord{\texttt{*}}a , m \rangle \longrightarrow \langle m(a) , m \rangle }\)

\(\inferrule[DoAssignVar]{ }{ \langle \mathord{\texttt{*}}a \mathrel{\texttt{=}} v , m \rangle \longrightarrow \langle v, m[a \mapsto v] \rangle }\)

\(\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 }\)

Inference Rules - Search Rules

\(\inferrule[SearchAssign]{ \langle e_2', m \rangle \longrightarrow \langle e_2', m' \rangle }{ \langle l_1 \mathrel{\texttt{=}} e_2 , m \rangle \longrightarrow \langle l_1 \mathrel{\texttt{=}} e_2' , m' \rangle }\)

\(\inferrule[SearchVarDecl]{ \langle e_1, m \rangle \longrightarrow \langle e_1', m' \rangle }{ \langle \mathbf{var}\;x\;\texttt{=}\;e_1\texttt{;}\;e_2 , m \rangle \longrightarrow \langle \mathbf{var}\;x\;\texttt{=}\;e_1'\texttt{;}\;e_2 , m' \rangle }\)

Implementation