This is a part of a series - start at the beginning.
This is just going to be a big pile of \( \LaTeX \). If you're not into that, check out the previous post where I explain the same things with pretty interactive repls instead.
\[ \gdef\D#1#2{\llbracket #1 \rrbracket_{#2}^E} \gdef\env{\mathsf{env}} \gdef\Denv#1{\D{#1}{\env}} \gdef\concat{\mathsf{concat}} \gdef\code#1{\textcolor{darkblue}{\texttt{#1}}} \]
Scalar values are integers or strings. Tuples are sequences of zero or more scalars. Values are sets of tuples.
\[ \begin{aligned} \mathsf{Scalar} &= \mathbb{Z} + \mathsf{String} \\ \mathsf{Tuple} &= \bigcup_{i \in \mathbb{N}} \mathsf{Scalar}^i \\ \mathsf{Value} &= 2^\mathsf{Tuple} \end{aligned} \]
Variable naming conventions:
\[ \code{imp code} \\ \mathsf{math} \\ \begin{aligned} \space\\ \code{N}, N &: \mathsf{Name} \\ \code{A}, \code{B} &: \mathsf{Expression} \\ a, b &: \mathsf{Tuple} \\ \code{s}, s &: \mathsf{Scalar} \\ n &: \N \\ \env &: \mathsf{Name} \rightarrow \mathsf{Value} \end{aligned} \]
I'll give the denotation first in terms of an environment function.
\[ \begin{aligned} \D{\cdot}{}&: (\mathsf{Name} \rightarrow \mathsf{Value}) \rightarrow \mathsf{Expression} \rightarrow \mathsf{Value} \\ \Denv{ \code{none} } &= \{\} \\ \Denv{ \code{some} } &= \{()\} \\ \Denv{ \code{s} } &= \{(s,)\} \\ \Denv{ \code{A | B} } &= \Denv{\code{A}} \cup \Denv{\code{B}} \\ \Denv{ \code{A \& B} } &= \Denv{\code{A}} \cap \Denv{\code{B}} \\ \Denv{ \code{A x B} } &= \{\mathsf{concat}(a, b) \mid a \in \Denv{\code{A}}, b \in \Denv{\code{B}}\} \\ \Denv{ \code{!A} } &= \text{if } \Denv{\code{A}} = \{\} \text{ then } \{()\} \text{ else } \{\} \\ \Denv{ \code{A = B} } &= \text{if } \Denv{\code{A}} = \Denv{\code{B}} \text{ then } \{()\} \text{ else } \{\} \\ \Denv{ \code{N} } &= \env(N) \\ \Denv{ \code{let N = A in B} } &= \D{ \code{B} }{ \mathsf{bind}(\env, N, \Denv{\code{A}}) } \\ \Denv{ \code{A B} } &= \{\concat(a[n+1..], b[n+1..]) \mid a \in \Denv{\code{A}}, b \in \Denv{\code{B}}, n = \mathsf{min}(\mathsf{len}(a), \mathsf{len}(b)), a[1..n] = b[1..n]\} \\ \Denv{ \code{N -> A} } &= \{ \mathsf{concat}((s,), a) \mid s \in \mathsf{Scalar}, a \in \D{\code{A}}{ \mathsf{bind}(\env, N, \{(s,)\}) } \} \end{aligned} \]
Finally:
\[ \begin{aligned} \D{\code{A}}{} &= \D{\code{A}}{N \mapsto \{\}} \end{aligned} \]
Note that these semantics allow undefined variables to have value \( \{\} \), but in practice we will produce a compile-time error instead.
Nothing surprising here, but it's good to have it written down explicitly. Next time we'll look at how to actually evaluate imp code.
Thanks to Michael Arntzenius for myriad corrections