Fixed Points and the Full Continuous Hierarchy
Our current motivation for studying domain-theoretic models is to construct Henkin models of typed lambda calculi with fixed-point operators.
The type frame, $\mathcal{A}$, called the full continuous $\lambda^{\times, \to}$ hierarchy over CPOs $\langle A^{b_0} ,\leq_0 \rangle , … , \langle A^{b_k} ,\leq_k \rangle$ is defined by taking $A^{b_0}, …, A^{b_k}$ as base types, and
\[\begin{split} &A^{\sigma \times \tau} = A^{\sigma} \times A^{\tau} \\ &A^{\sigma \to \tau} = \text{ all continuous } f: \langle A^{\sigma} ,\leq_\sigma \rangle \to \langle A^{\tau} ,\leq_\tau \rangle \end{split}\]with $A^{\sigma \times \tau}$ ordered coordinate-wise by $\leq_{\sigma \times \tau}$ and $A^{\sigma \to \tau}$ ordered point-wise by $\leq_{\sigma \to \tau}$. By Lemma 1 and Lemma 4 in the last article, each $\langle A^{\sigma} ,\leq_\sigma \rangle$ is a CPO.
The main result of this section is that the full continuous type hierarchy over any CPOs forms a Henkin model, with least-fixed-point operators at all pointed types. Before proving that the full continuous hierarchy is a Henkin model, we consider the interpretation of $fix$.
We say $a$ is a least fixed point of $f$ if $a = f(a)$ and, whenever $b = f(b)$, we have $a \leq b$.
(Lemma 1.) If $\mathcal{D}$ is a pointed CPO, and $f:\mathcal{D} \to \mathcal{D}$ is continuous, then $f$ has a least fixed point
\[fix_D \: f = \bigvee \{ f^n(\perp) \mid n \geq 0 \}.\]In addition, the map $fix_D$ is a continuous function.
This lemma says that we can find the least fixed point of any function $f$ by repreatedly applying $f$ to the least element of its domain. This lemma is also called the Kleene fixed-point theorem, see this wiki page for more information.
(Proof.) Let $f:\mathcal{D} \to \mathcal{D}$ be continuous. Since $f$ is monotonic, and $\perp \leq f(\perp)$, we can see that $f^n(\perp) \leq f^{n+1}(\perp)$. It follows that \(\{ f^n(\perp) \mid n \geq 0 \}\) is linearly ordered and therefore directed. Let $a$ be the least upper bound \(a = \bigvee \{ f^n(\perp) \mid n \geq 0 \}\).
We must show that $a$ is a fixed point of $f$. By continuity of $f$,
\[\begin{split} f(a) &= f(\bigvee \{ f^n(\perp) \mid n \geq 0 \})\\ &= \bigvee \{ f^{n+1}(\perp) \mid n \geq 0 \}. \end{split}\]Since \(\{ f^n(\perp) \mid n \geq 0 \}\) and \(\{ f^{n+1}(\perp) \mid n \geq 0 \}\) have the same least upper bound, we have $f(a) = a$.
To see that $a$ is the least fixed point of $f$, suppose $b = f(b)$ is any fixed point. Since $\perp \leq b$, we have $f(\perp) \leq f(b)$ and similarly $f^n(\perp) \leq f^n(b)$ for any $n \geq 0$. But since $b$ is a fixed point of $f$, $f^n(b) = b$. Therefore $b$ is an upper bound for the set \(\{ f^n(\perp) \mid n \geq 0 \}\). Since the least upper bound of this set is $a$, it follows that $a \leq b$.
The final step is to show that the function $fix_D$ mapping $f$ to \(\{ f^n(\perp)\}\) is itself continuous. Let us suppose that $S \subseteq D \to D$ is directed, with $\bigvee S = f$. We must show that \(fix_D \: f = \bigvee \{ fix_D \: g \mid g \in S \}\). By continuity of function application, each $f^n(\perp)$ is the least upper bound of the set of all $g^n(\perp)$ with $g \in S$. Therefore,
\[\begin{split} fix_D \: f &= \bigvee \{ f^n(\perp) \mid n \geq 0 \}\\ &= \bigvee \{ g^{n}(\perp) \mid n \geq 0 ,\: g \in S \}. \end{split}\]It is easy to see that \(\{ g^{n}(\perp) \mid n \geq 0 ,\: g \in S \}\) and \(\{ fix_D \: g \mid g \in S \}\) have the same least upper bound, since any upper bound for the $g^n(\perp)$’s must be an upper bound for the \((fix_D \: g)\)’s. Therefore,
\[fix_D \: f = \bigvee \{ fix_D \: g \mid g \in S \}.\]This proves the lemma. $\blacksquare$
A trivial example is $fix$ $id$, where $id:\mathcal{D} \to \mathcal{D}$ is the identity function on the pointed CPO $\mathcal{D}$. We can calculate the least fixed point of $id$ as follows.
\[\begin{split} fix \: id &= \bigvee \{ id^n(\perp_D) \mid n \geq 0 \} \\ &= \bigvee \{ \perp_D \} \\ &= \perp_D \end{split}\]This calculation clearly gives the right answer, since $\perp$ is a fixed point of the identity function, and no element of $\mathcal{D}$ is less than $\perp$.
A Theorem
In this section, we show that the full continuous hierarchy is a Henkin model. The following two lemmas are essential to the inductive proof of the envrionment model condition.
(Lemma 2.) If $f : \mathcal{C} \to (\mathcal{D} \to \mathcal{E})$ and $g: \mathcal{C} \to \mathcal{D}$ are continuous, then so is the function \(App \: f \: g\) given by
\[(App \: f \: g) \: c = (f\:c)\:(g\:c)\]for all $c in \mathcal{C}$. In addition, the map $App$ is continuous.
(Lemma 3.) If $f : \mathcal{C} \times \mathcal{D} \to \mathcal{E}$ is continuous, then there is a unique continuous function \((Curry \: f):\mathcal{C} \to (\mathcal{D} \to \mathcal{E})\) such that for all $c \in C$ and $d \in D$, we have
\[(Curry \: f) \: c \: d = f \: \langle c,d \rangle.\]In addition, the map $Curry$ is continuous.
(Proof of Lemma 2.) The monotonicity of \(App \: f \: g\) and of $App$ itself is easy to prove.
We then show that \(App \: f \: g\) is continuous. If $S \subseteq C$ is directed, then we can make the following calculation:
\[\begin{split} \bigvee \{ (App \: f \: g) \: c \mid c \in S \} &= \bigvee \{ (f \: c) \: (g \: c) \mid c \in S \} \\ &= (\bigvee \{ f \: c \mid c \in S \}) \: (\bigvee \{ g \: c \mid c \in S \}) \text{ by continuity of application}\\ &= f(\bigvee S ) \: g(\bigvee S) \text{ by continuity of } f,g\\ &= (App \: f \: g)\:(\bigvee S ) \end{split}\]To show that $App$ itself is continuous, suppse $S_1 \subseteq (C \to D \to E)$ and $S_2 \subseteq (C \to D)$ are directed. We can check continuity by this calculation:
\[\begin{split} \bigvee \{ App \: f \: g \mid f \in S_1, \: g \in S_2 \} &= \bigvee \{ c \mapsto (f \: c) \: (g \: c) \mid f \in S_1, \: g \in S_2 \} \\ &= c \mapsto \bigvee \{(f \: c) \: (g \: c) \mid f \in S_1, \: g \in S_2 \} \text{ by Lemma 4 in the last article}\\ &= c \mapsto (\bigvee \{ f \: c \mid f \in S_1 \}) \: (\bigvee \{ g \: c \mid g \in S_2 \}) \text{ by continuity of application}\\ &= c \mapsto ((\bigvee S_1)\:c) \: ((\bigvee S_2)\:c) \text{ by continuity of application}\\ &= App \: (\bigvee S_1) \: (\bigvee S_2) \end{split}\]We use the symbol $\mapsto$ to represent the mathematical function (mapping), differentiating from the function type symbol $\to$ in lambda calculus.
This proves the lemma. $\blacksquare$
(Proof of Lemma 3.)
The monotonicity is easy to prove.
To show that $Curry : f$ is continuous, we assume that $S \subseteq C$ is directed. Using the similar reasoning as in the proof of Lemma 2, we have the following continuity calculation:
\[\begin{split} \bigvee \{ (Curry \: f) \: c \mid c \in S \} &= \bigvee \{ d \mapsto f \: \langle c,d \rangle \mid f \in S \} \\ &= d \mapsto \bigvee \{f \: \langle c,d \rangle \mid c \in S \} \text{ by Lemma 4 in the last article}\\ &= d \mapsto f \: \langle \bigvee S,d \rangle \text{ by continuity of pairing}\\ &= (Curry \: f) \: \bigvee S \end{split}\]To show that $Curry$ itself is continuous, we assume that $S \subseteq (C \times D \to E)$ is directed and make a similar calculation:
\[\begin{split} \bigvee \{ Curry \: f \mid f \in S \} &= \bigvee \{ c \mapsto d \mapsto f \: \langle c,d \rangle \mid f \in S \} \\ &= c \mapsto \bigvee \{ d \mapsto f \: \langle c,d \rangle \mid f \in S \} \text{ by Lemma 4 in the last article}\\ &= c \mapsto ( d \mapsto \bigvee \{ f \: \langle c,d \rangle \mid f \in S \}) \text{ by Lemma 4 in the last article}\\ &= c \mapsto ( d \mapsto (\bigvee S) \: \langle c,d \rangle ) \text{ by continuity of pairing}\\ &= Curry \: (\bigvee S) \end{split}\]This proves the lemma. $\blacksquare$
We now show that the full continuous hierarchy is a Henkin model.
(Lemma 4.) The full continuous hierarchy over any collection of CPOs is a Henkin model.
(Proof.) It is easy to see that the full continuous hierarchy for $\lambda^{\times, \to}$ is an extensional applicative structure.
We prove that the environment model condition is satisfied using an induction hypothesis that is slightly stronger than the theorem. Specifically, in addition to showing that the meaning of every term exists, we show that the meaning is a continuous function of values assigned to free variables by the environment. We use the assumption that meanings are continuous to show that a function defined by lambda abstraction is continuous.
We say \([\![ \Gamma \: \triangleright \: M:\tau ] \!]\) is continuous if, for every $x:\sigma \in \Gamma$ and $\eta \vDash \Gamma$, the map
\[a \in A^\sigma \mapsto [\![ \Gamma \: \triangleright \: M:\tau ] \!]\eta[x \mapsto a]\]is a continuous function from $A^\sigma$ to $A^\tau$.
This is the same as saying \([\![ \Gamma \: \triangleright \: M:\tau ] \!]\) is continuous as an $n$-ary function $A^{\sigma_1} \times … \times A^{\sigma_n} \to A^\tau$, where \(\Gamma = \{ x_1,\sigma_1, ..., x_n,\sigma_n\}\).
Using Lemma 2 and Lemma 3, the inductive proof is straightforward. It is easy to see that
\[[\![x_1,\sigma_1, ..., x_n,\sigma_n \: \triangleright \: x_i:\sigma_i]\!]\eta = \eta(x_i)\]is continuous, since identity and constant functions are continuous, and similarly for the meaning of a constant symbol. For application, we use Lemma 2, and for lambda abstraction, Lemma 3. $\blacksquare$
We have the following theorem, as a consequence of Lemma 1 and Lemma 4.
(Theorem 1.) The full continuous $\lambda^{\times,\to}$ hierarchy $\mathcal{A}$ over any collection of CPOs is a Henkin model with the property that whenever $A^\sigma$ is pointed there is a least fixed point operator $fix_\sigma \in A^{\sigma \to \sigma}$.
Recall that if $A^\tau$ is pointed (has a least element), then $A^{\sigma \to \tau}$ is pointed and if both $A^\sigma$ and $A^\tau$ are pointed, then $A^{\sigma \times \tau}$ is pointed. In particular, if we choose pointed CPOs for the type constants, then every $A^\sigma$ will be pointed and we will have least-fixed-point operators at all types. We consider a specific case, a CPO model for PCF, in the next article.