Denotational Semantics
What questions do you have? What questions does your neighbor have?
Announcements
- This Thursday: Theorem Proving in Lean with Kirby
Questions?
Review: Them’s Just Semantics
An operational semantics is …
An axiomatic semantics is …
A denotational semantics is …
Review: Denotations
We define a (compilation) function \(\lbrack\!\lbrack\cdot \rbrack\!\rbrack\) on syntax to its denotation. A denotation is something in the meta logic (e.g., sets, functions, partial-ordered sets, complete lattices, monotone functions, continuous functions).
Exercise: Denotational Semantics of Expressions
Define a denotation \(\lbrack\!\lbrack e \rbrack\!\rbrack\) by induction on the structure of \(e\) to a function from stores to values \(\lambda \rho.v\), that is, \(\lbrack\!\lbrack e \rbrack\!\rbrack : \operatorname{Store}\rightarrow \operatorname{Val}\) where \(\rho: \operatorname{Store}\) and \(v: \operatorname{Val}\).
Denotational Semantics of Expressions
\[ \fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack = \lambda \rho.v$} \]
\[ \begin{array}{rrl} \lbrack\!\lbrack x \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \rho(x) \\ \lbrack\!\lbrack e_1 \mathbin{\texttt{+}} e_2 \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \lbrack\!\lbrack e_1 \rbrack\!\rbrack\,\rho + \lbrack\!\lbrack e_2 \rbrack\!\rbrack\,\rho \end{array} \]
Denotational Semantics of Expressions
\[ \fbox{$\lbrack\!\lbrack e \rbrack\!\rbrack{\rho} = v$} \]
\[ \begin{array}{rrl} \lbrack\!\lbrack x \rbrack\!\rbrack\,\rho & \mathrel{:=}& \rho(x) \\ \lbrack\!\lbrack e_1 \mathbin{\texttt{+}} e_2 \rbrack\!\rbrack\,\rho & \mathrel{:=}& \lbrack\!\lbrack e_1 \rbrack\!\rbrack\,\rho + \lbrack\!\lbrack e_2 \rbrack\!\rbrack\,\rho \end{array} \]
Exercise: Denotational Semantics of Statements
Define a denotation \(\lbrack\!\lbrack s \rbrack\!\rbrack\) by induction on the structure of \(s\) to a function from stores to stores \(\lambda \rho.\rho'\), that is, \(\lbrack\!\lbrack s \rbrack\!\rbrack : \operatorname{Store}\rightarrow \operatorname{Store}\).
Denotational Semantics of Statements
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack = \lambda \rho.\rho'$} \]
\[ \begin{array}{rrl} \lbrack\!\lbrack \texttt{;} \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \rho \\ \lbrack\!\lbrack s_1 \mathbin{\texttt{;}} s_2 \rbrack\!\rbrack & \mathrel{:=}& \lbrack\!\lbrack s_2 \rbrack\!\rbrack \circ \lbrack\!\lbrack s_1 \rbrack\!\rbrack \\ \lbrack\!\lbrack \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho = \mathbf{true}\,\operatorname{then}\, \lbrack\!\lbrack s_1 \rbrack\!\rbrack\,\rho \,\operatorname{else}\, \lbrack\!\lbrack s_2 \rbrack\!\rbrack\,\rho \\ \lbrack\!\lbrack x \mathrel{\texttt{=}}e \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \rho(x \leftarrow \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho ) \end{array} \]
Exercise: Denotational Semantics: While
\[ \begin{array}{rrl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack & \mathrel{:=}& ??? \end{array} \]
Denotational Semantics: While
\[ \begin{array}{rrrl} \text{store or don't know} & \mathring{\rho}: \mathring{\operatorname{Store}}& \mathrel{::=}& \rho\mid\bot \end{array} \]
Think of \(\bot\) here as “don’t know yet” or “out of fuel”.
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack = \lambda \mathring{\rho}.\mathring{\rho}'$} \]
\[ \begin{array}{rrl} \lbrack\!\lbrack s \rbrack\!\rbrack & \mathrel{:=}& \lambda \bot.\bot \\ \lbrack\!\lbrack \texttt{;} \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \rho \\ \lbrack\!\lbrack s_1 \mathbin{\texttt{;}} s_2 \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \lbrack\!\lbrack s_2 \rbrack\!\rbrack\, (\lbrack\!\lbrack s_1 \rbrack\!\rbrack\,\rho) \\ \lbrack\!\lbrack \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho = \mathbf{true}\,\operatorname{then}\, \lbrack\!\lbrack s_1 \rbrack\!\rbrack\,\rho \,\operatorname{else}\, \lbrack\!\lbrack s_2 \rbrack\!\rbrack\,\rho \\ \lbrack\!\lbrack x \mathrel{\texttt{=}}e \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \rho(x \leftarrow \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho ) \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \operatorname{if}\, \text{$\lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack_{k}\,\rho \neq \bot$ for some $k$} \,\operatorname{then}\, \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack_{k}\,\rho \,\operatorname{else}\, \bot \end{array} \]
\[ \fbox{$\lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack_{i} = \lambda \mathring{\rho}.\mathring{\rho}'$} \]
\[ \begin{array}{lrl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack_{i} & \mathrel{:=}& \lambda \bot.\bot \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack_{0} & \mathrel{:=}& \lambda \rho.\bot \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack_{i + 1} & \mathrel{:=}& \lambda \rho. \operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho = \mathbf{true}\,\operatorname{then}\, \lbrack\!\lbrack\mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack_{i}\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\rho) \,\operatorname{else}\, \rho \end{array} \]
Store Transformers
\[ \begin{array}{rlrl} \text{store transformer (i.e., transfer function)} & f: \mathring{\operatorname{Store}} \rightarrow \mathring{\operatorname{Store}}& \mathrel{::=}& \lambda \mathring{\rho}.\mathring{\rho}' \\ \text{store transformer functional} & F: (\mathring{\operatorname{Store}} \rightarrow \mathring{\operatorname{Store}}) \rightarrow (\mathring{\operatorname{Store}} \rightarrow \mathring{\operatorname{Store}}) & \mathrel{::=}& \lambda f.f' \end{array} \]
Unwinding Equation
\[ \begin{array}{rcl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack & = & \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, \lbrack\!\lbrack\mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot \end{array} \]
Why can’t we use this as a definition?
Fixed Points
\[ \begin{array}{rcl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack & = & \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, \lbrack\!\lbrack\mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot \\ \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack & = & F_{\mathbf{while}\texttt{(}e\texttt{)}s}(\lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s \rbrack\!\rbrack) \\ F_{\mathbf{while}\texttt{(}e\texttt{)}s} & \mathrel{:=}& \lambda f. \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, f\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot \end{array} \]
We want to pick a specific fixed point of \(F_{\mathbf{while}\texttt{(}e\texttt{)}s}\).
Ordering Transformers
Order store transfomers by most “don’t know yet”.
\[ \begin{array}{rcl} f_1 \sqsubseteq f_2 & \text{iff} & \text{$f_1(\mathring{\rho}) = \bot$ or $f_1(\mathring{\rho}) = f_2(\mathring{\rho})$} \quad\text{for all $\mathring{\rho}$} \end{array} \]
Fixed-Point Theorems
Theorem 1 (Kleene Fixed-Point Theorem) Let \(P\) be a complete partial order and \(k : P \rightarrow P\) be a continuous function. Then, \(k\) has a least fixed point that can be computed as follows: \[ \begin{array}{rcl} \operatorname{lfp}\,k & = & \bigsqcup_i k^i(\bot) \end{array} \]
Theorem 2 (Tarski-Knaster Fixed-Point Theorem) Let \(L\) be a complete lattice and \(m : L \rightarrow L\) be a monotone function. Then, \(m\) has a least fixed point.
Denotational Semantics: While: Fixed Points
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack = \lambda \mathring{\rho}.\mathring{\rho}'$} \]
\[ \begin{array}{rrl} \lbrack\!\lbrack s \rbrack\!\rbrack & \mathrel{:=}& \lambda \bot.\bot \\ \lbrack\!\lbrack \texttt{;} \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \rho \\ \lbrack\!\lbrack s_1 \mathbin{\texttt{;}} s_2 \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \lbrack\!\lbrack s_2 \rbrack\!\rbrack\, (\lbrack\!\lbrack s_1 \rbrack\!\rbrack\,\rho) \\ \lbrack\!\lbrack \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho = \mathbf{true}\,\operatorname{then}\, \lbrack\!\lbrack s_1 \rbrack\!\rbrack\,\rho \,\operatorname{else}\, \lbrack\!\lbrack s_2 \rbrack\!\rbrack\,\rho \\ \lbrack\!\lbrack x \mathrel{\texttt{=}}e \rbrack\!\rbrack & \mathrel{:=}& \lambda \rho. \rho(x \leftarrow \lbrack\!\lbrack e \rbrack\!\rbrack\,\rho ) \\ \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack & \mathrel{:=}& \operatorname{lfp}\,(\lambda f. \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, f\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot ) \end{array} \]
Denotational Semantics: While with While
\[ \fbox{$\lbrack\!\lbrack s \rbrack\!\rbrack = \lambda \mathring{\rho}.\mathring{\rho}'$} \]
\[ \begin{array}{rrl} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack & \mathrel{:=}& \operatorname{lfp}\,(\lambda f. \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, f\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot ) \end{array} \]
\[ \text{or} \]
\[ \begin{array}{l} \lbrack\!\lbrack \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rbrack\!\rbrack \quad \mathrel{:=} \\ \qquad\operatorname{let}\,F = (\lambda f. \lambda \mathring{\rho}. \operatorname{if}\, \mathring{\rho}\neq \bot \,\operatorname{then}\, (\operatorname{if}\, \lbrack\!\lbrack e \rbrack\!\rbrack\,\mathring{\rho} = \mathbf{true}\,\operatorname{then}\, f\,(\lbrack\!\lbrack s \rbrack\!\rbrack\,\mathring{\rho}) \,\operatorname{else}\, \mathring{\rho}) \,\operatorname{else}\, \bot ); \\ \qquad f \leftarrow \bot; \mdowhile {f' \leftarrow F\,f} { f\sqsubseteq f' }; \\ \qquad f \end{array} \]
Collecting Semantics
Them’s Just Semantics
An operational semantics is …
An axiomatic semantics is …
A denotational semantics is …
A collecting semantics is …
Verification as Reachability
We want to collect all reachable states — properties.
\[ \begin{array}{rr} \text{store properties} & P& \mathrel{::=}& \circ\mid P,\rho \end{array} \]
That is, we want to define a collecting semantics \(\lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace = \lambda P.P'\) for the forward state-reachability property. That is, we want the following equation to hold:
\[ \lbrace\!\lbrack\!\lbrack s \rbrack\!\rbrack\!\rbrace{P} = \{ \rho' \mid \text{$\rho \vdash s \Downarrow\rho'$ for all $\rho\in P$} \} \]