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
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}$.
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$.