As the last article of this series, today we will discuss the denotational semantics for imperative programs. Specifically, we will check out how to apply CPO model on the $\text{while}$ programs introduced in Easy Foundations for Programming Languages X — Imperative Programs.
Typed Lambda Calculus with Stores
Basic Structure
We will give a denotational semantics for $\text{while}$ programs using a typed lambda calculus with locations and stores, which we interpret over CPOs.
The lambda calculus we use, which resembles PCF with locations and stores added, will be refered to as $\lambda^{store,fix,\to}$. This calculus has type constants $val$, $bool$, $loc$, $store$, and $store_{\perp}$, with the first four interpreted as in the algebra $\mathcal{A}$. The difference between $store$ and $store_{\perp}$ is that the latter will have an added least element, $\perp_{store}$.
Recall that a value of type $store$ represents the “memory contents” of some simple machine. Hence, $\perp_{store}$ depicts a kind of machine state where the program cannot terminate.
In addition to function symbols from the signature $\Sigma$, giving functions on $val$ and $bool$, the calculus $\lambda^{store,fix,\to}$ has an equality test
\[\phantom{\stackrel{\text{def}}{=}}Eq?:loc \to loc \to bool\]on locations, store operations $init$, $update$ and $lookup$, a conditional $\text{if } … \text{ then } … \text{ else }…$ of each type. as in PCF, lifting operations (described below), lambda abstraction, application, and a fixed-point operator $fix_{store}$ of type
\[fix_{store}:((store \to store_\perp) \to (store \to store_\perp)) \to (store \to store_\perp).\]This will be used to define functions from $store$ to $store_\perp$ recursively.
The CPO model, $\mathcal{A}_\lambda$, for $\lambda^{store,fix,\to}$ will be an extension of the four-sorted algebra, $\mathcal{A}$, that was constructed by extending $\mathcal{A}_0$ with locations and stores.
Since any set may be regarded as a discrete CPO, we may continue to interpret $val$, $bool$, $loc$ and $store$ as in $\mathcal{A}$.
We interpret $store_\perp$ as the lifted set \(A^{store_\perp}=(A^{store})_\perp\), and extend to function types by letting $A^{\sigma \to \tau}$ be all continuous functions from $A^\sigma$ to $A^\tau$, ordered point-wise. Since $A^{store_\perp}$ is pointed $A^{store \to store_\perp}$ is also pointed. By Theorem 1 in Denotational Semantics of Typed Lambda Calculus III — Full Continuous Hierarchy, this continuous hierarchy has a least fixed-point operator of the required type.
The operations associated with $store_\perp$ are a map from $store$ to $store_\perp$, which we write \(\lfloor \: \cdot \:\rfloor\). If $M:store$, then \(\lfloor M \rfloor:store_\perp\) denotes the same store as $M$, but regarded as an element of the lifted set of stores, $A^{store}_\perp$.
The other operation is a strict form of function application, which we write as an infix operator, $\cdot$. To be precise, we give a typing rule for this operation.
\[\frac{\Gamma \:\triangleright \: M : store \to store_{\perp},\: \Gamma \:\triangleright \: N : store_{\perp}}{\Gamma \:\triangleright \: M \cdot N : store_{\perp}} \tag*{($store_{\perp}$ Elim)}\]The semantics interpretation of $\cdot$ is that if $N$ is $\perp$, then $M \cdot N$ is $\perp$, and otherwise $M \cdot N$ is the result of applying $M$ to the denotation of $N$, which must belong to $A^{store}$.
Two equational axioms associated with these operations are
\[\begin{split} \Gamma \: \triangleright \: M \cdot \perp &= \perp : store_\perp \\ \Gamma \: \triangleright \: M \cdot \lfloor N \rfloor &= M \: N : store_\perp . \end{split}\]It is easy to check that strict application, $\cdot$, is continuous in both arguments. And it is useful to define a strict form of function composition as syntactic sugar, by
\[M \diamond N \stackrel{\text{def}}{=} \lambda s : store.M \cdot (N \: s).\]Explain
To give some idea of how $\lambda^{store, fix, \to}$ will be used, recall that according to the operational semantics, executing an assignment statement $x := 3$ updates the store so that the contents of $x$ becomes $3$. If we ignore the difference between location variables and the location they denote, then the operational semantics might be written
\[\langle x,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} update^\mathcal{A} (s, x, 3).\]Recall that the notation \(\langle M,\: s \rangle \stackrel{\text{eval}}{_\rightsquigarrow} v\) means that we “evaluate” expression $M$ in store $s$ and obtain value $v$; and the function \(update: store \times loc \times val \to store\) changes the value associated with some location and return the changed stores.
Put another way, executing $x := 3$ maps any store $s$ to the store $update^\mathcal{A} (s, x, 3)$. In the lambda calculus of locations and stores, we may write this function on stores as
\[\lambda s: store.update \: s \: x \: 3.\]Note that this lambda expression is well-typed, since the typing constraints on assignment requires $x:loc$. A technical detail is that this is a function from $store$ to $store$, and $A^{store}$ has no least element. Since the $\text{while}$ program may not terminate, the type of lambda term giving the meaning of a program must be $store \to store_\perp$, instead of $store \to store$. Therefore, we write the meaning of the assignment as the lambda expression
\[\lambda s:store. \lfloor update \: s \: x \: 3 \rfloor .\]For any $\text{while}$ program $S$, we will be able to write a $\lambda^{store, fix, \to}$ expression for the mapping from $store$ to $store_\perp$ given by the execution rules for $S$. We will use stores and associated operations for assignment and variable access, as illustrated here, strict composition for sequence of statements, and fixed points for iteration ($\text{while}$ loops).
Reason of Strict Composition
The use of strict composition may appear accidental, but it is actually essential. This may be understood by considering a sequence such as \(P; \: x:=3\). The meaning of this program will be given by the strict composition, $g \diamond f$, of the function $f$ from $store$ to $store_\perp$ determined by $P$ and the function $g$ from $store$ to $store_\perp$ determined by $x := 3$.
If we use functions $f$ and $g$ from $store_\perp$ to $store_\perp$, and ordinary composition instead, then we have the following problem. Suppose that when we begin in store $s$, program $P$ does not terminate. Since the least element $\perp$ of a CPO is used to give a mathematical value to a nonterminating computation, the meaning of $P$ would be a function $f$ with \(f \:s = \perp_{store}\). Since \(P; \: x:=3\) cannot terminate (operationally) if $P$ does not, the meaning of \(P; \: x:=3\) should maps $s$ to $\perp_{store}$.
But if we treated stores as functions from locations to values and used a nonstrict update function
\[update_{non-strict} \: s \: x \: v \stackrel{\text{def}}{=} \lambda y:loc.\text{if } Eq? \: y \: x \text{ then } v \text{ else } lookup \: s' \: y\]then $(g \circ f)(s)$ could be some store different from $\perp$ which in fact contained a value for $x$. This would cause both the equivalence between operational and denotational semantics and the soundness of the proof rules for the denotational semantics to fail. We therefore use strict composition to guarantee that the meaning of a sequence $P;Q$ yields $\perp$ whenever the meaning of $P$ yields $\perp$.
Semantic Functions
Definitions
There are two main parts of the denotational semantics of $\text{while}$ programs. The first is a syntactic translation of expressions and commands into lambda terms of $\lambda^{store,fix,\to}$, and the second is the standard interpretation of this lambda calculus in the model $\mathcal{A}_\lambda$.
We use the function \(\mathcal{V} [\![ \: \cdot \: ]\!]\) to translate boolean and value expressions of $\text{while}$ programs into lambda terms of type $store \to bool$ and $store \to val$, respectively. If $M:val$ is an expression that might occur on the right side of an assignment, the translation \(\mathcal{V} [\![ M ]\!]\) will be a lambda term of type $store \to val$ with the same free variables.
The function \(\mathcal{C} [\![ \: \cdot \: ]\!]\) is a similar translation from commands to lambda terms of type $store \to store_\perp$.
Combining these two translations with the ordinary meaning function from $\lambda^{store, fix, \to}$ to the model $\mathcal{A}_\lambda$, we obtain two functions
\[\begin{split} &\overline{\mathcal{V}}: expressions \to environments \to store \to values \\ &\overline{\mathcal{C}}: commands \to environments \to store \to store_\perp \end{split}\]where “values” is used here to indicate that expressions may have type $val$ and $bool$.
In the jargon of denotational semantics, $\overline{\mathcal{V}}$ and $\overline{\mathcal{C}}$ are called semantic functions. These functions make dependence on the store explicit: an algebraic expression of sort $val$ becomes a function from stores to values, and commands become mapping from stores to stores.
We now define the syntactic translation and semantic function for expressions. Essentially, $\mathcal{V} [![ M ]!]$ is defined by replacing the content function symbol $cont$ with $lookup$ and treating the $store$ explicitly.
\[\begin{split} \mathcal{V} [\![ x ]\!] &= \lambda s: store . x\\ \mathcal{V} [\![ cont \: x ]\!] &= \lambda s: store . lookup \: s \: x\\ \mathcal{V} [\![ f \: M_1 \: ... \: M_k ]\!] &= \lambda s: store . f \: \mathcal{V} [\![ M_1 ]\!] s \: ... \: \mathcal{V} [\![ M_k ]\!] s \end{split}\]We use the symbol \(\overline{\mathcal{V}} [\![ M ]\!] \eta\) to represent the meaning of expression $\boldsymbol{M}$ in environment $\boldsymbol{\eta}$. In principle, we have
\[\overline{\mathcal{V}} [\![ M ]\!] \eta = \mathcal{A}_\lambda [\![ \: \mathcal{V}[\![ M ]\!] \: ]\!] \eta.\]Since the meaning of a value expression $M:val$ in $\eta$ is a function from stores to values, we may find the value \(\overline{\mathcal{V}} [\![ M ]\!] \eta\) of $M$ in environment $\eta$ and store $s \in A^{store}$ by function application
\[\overline{\mathcal{V}} [\![ M ]\!] \eta \: s = (\overline{\mathcal{V}} [\![ M ]\!] \eta) \: (s) .\]Note that since our language does not allow calls to recursive functions in expressions, we do not need lifted types of values in defining $\mathcal{V}$.
The syntactic translation of a command produces a lambda term mapping $store$ to $store_\perp$. The effect of an assignment is to update the store. A sequence of commands denotes the strict composition of corresponding maps on stores, and the semantics of conditional is essentially straightforward. The semantics of $\text{while}$ is the fixed-point of a functional described in more detail below.
\[\begin{split} \mathcal{C} [\![ x:=M ]\!] =& \lambda s:store. \lfloor update \: s \: x \: (\mathcal{V} [\![ x:=M ]\!] s) \rfloor \\ \mathcal{C} [\![ P_1;P_2 ]\!] =& \mathcal{C} [\![ P_1 ]\!] \diamond \mathcal{C} [\![ P_2 ]\!] \\ \mathcal{C} [\![\text{if } B \text{ then } P_1 \text{ else } P_2]\!] =& \lambda s:store. \text{if } \mathcal{V} [\![ B ]\!] s \text{ then } \mathcal{V} [\![ P_1 ]\!] s \text{ else } \mathcal{V} [\![ P_2 ]\!] s\\ \mathcal{C} [\![\text{while } B \text{ do } P \text{ od} ]\!] =& fix (\lambda f:store \to store_\perp.\\ &\lambda s:store .\text{if } \mathcal{V} [\![ B ]\!] s \text{ then } f \diamond \mathcal{V} [\![ P ]\!] s \text{ else }\lfloor s \rfloor)\\ \end{split}\]The meaning of program $\boldsymbol{P}$ in environment $\boldsymbol{\eta}$ is defined by
\[\overline{\mathcal{C}} [\![ P ]\!] \eta = \mathcal{A}_\lambda [\![ \: \mathcal{C}[\![ P ]\!] \: ]\!] \eta.\]and the meaning in environment $\eta$ and store $s \in A^{store}$ by
\[\overline{\mathcal{C}} [\![ P ]\!] \eta \: s = (\overline{\mathcal{C}} [\![ P ]\!] \eta) \: (s) .\]Intuitively, there are two cases to consider in understanding the meaning of \(\text{while } B \text{ do } P \text{ od}\). If $B$ is false, then the command terminates in the same store as it started. If $B$ is true, then $P$ is executed, and the entire process is repeated. Consequently, the command \(\text{while } B \text{ do } P \text{ od}\) denotes the function $f$ from stores to stores satisfying
\[f \: s = \text{if } \mathcal{V} [\![ B ]\!] s \text{ then } \mathcal{V} [\![ P_1 ]\!] s \text{ else } \mathcal{V} [\![ P_2 ]\!] s.\]The equation may be understood by noting that if $B$ is false in the initial store $s$, the function returns the same store (regarded as an element of $store_\perp$). If $B$ is true, $f$ is applied to the store obtained as a result of “executing” $P$.
Another way of understanding the fixed-point interpretation of $\text{while}$ is by $fix$ reduction, which we consider in the following example.
Example
One simple program is
\[skip \stackrel{\text{def}}{=} x:= cont \: x\]where $x$ is some location variable. This program does nothing in our semantics, a fact that is proved in following three steps.
\[\begin{split} \mathcal{C} [\![ skip ]\!] =& \lambda s: store. \lfloor update \: s \: x \: (\mathcal{V} [\![ x ]\!]s) \rfloor \\ =& \lambda s: store. \lfloor update \: s \: x \: (lookup \: s \: x) \rfloor \\ =& \lambda s: store. \lfloor s \rfloor \\ \end{split}\]In the above second step, we use the algebraic axiom $(update)_1$ for $lookup$ and $update$.
The result of executing $skip$ in environment $\eta$ and store $s$ is given by $\overline{\mathcal{C}}$ as follows.
\[\begin{split} \overline{\mathcal{C}} [\![ skip ]\!] \eta \: s =& (\mathcal{A} [\![ \: \mathcal{C}[\![ skip ]\!] \: ]\!] \eta) (s) \\ =& (\mathcal{A} [\![ \: \lambda s:store. \lfloor s \rfloor \: ]\!] \eta) (s) \\ =& \lfloor s \rfloor\\ \blacksquare \end{split}\]We should note that the assignment \(x:=cont \: x\) does not denote the identity map in every programming language. For example, in a language with variable declarations and storage allocation, \(x:=cont \: x\) might produce an error if $x$ is undeclared.