Recall the untyped \lambda calculus:
We mentioned before that the semantic domain of this language must be a cpo D such that D \simeq D\twoheadrightarrow D In other words, solutions to this equation are fixed points of \mathcal {F}(X) = X\twoheadrightarrow X. The least such fixed point can expressed, by Theorem [dt-005B], as the colimit of the \omega -chain:
But, the least solution to this equation is trivial: D_\infty \simeq \mathbf {1}, because \mathbf {1} \simeq \mathbf {1}\twoheadrightarrow \mathbf {1}. A non-trivial solution is obtained by starting the chain at \mathbf {2}, the cpo containing just \{\top ,\bot \}, rather than \mathbf {1}.
We will now sketch a proof of the retraction pair between D_\infty and D_\infty \twoheadrightarrow D_\infty , by providing two functions, \textbf {\textsf {up}} : D_\infty \rightarrow (D_\infty \twoheadrightarrow D_\infty ) and its inverse \textbf {\textsf {down}} : (D_\infty \twoheadrightarrow D_\infty ) \rightarrow D_\infty .
Observe that each element of D_i (for i > 0) is a function D_{i-1} \twoheadrightarrow D_{i-1}. Therefore, an element of the colimit D_\infty is an \omega -tuple of such functions. To define \textbf {\textsf {up}}(d)(x), we must essentially "apply" each function in the element d \in D_\infty (viewed as an \omega -tuple of functions) to the element x \in D_\infty (viewed as an \omega -tuple of values). More specifically, we say that \textbf {\textsf {up}}(d)(x) is an \omega -tuple (y_m \mid y \in \mathbb {N}), as follows:
y_m = \bigsqcup _{k \in \mathbb {N}} \theta _{m+k,m}(d_{m+k+1}(x_{m+k}))
To define \textbf {\textsf {down}}(f), we are given a (continuous) function f : D_\infty \twoheadrightarrow D_\infty and must construct the \omega -tuple of approximations at every D_n. We do this by projecting the action of f down to D_n. We say that \textbf {\textsf {down}}(f) is an \omega -tuple (v_n \mid n \in \mathbb {N}) where:
\begin {array}{lcl}
v_0 & \triangleq & \theta _{\infty ,0}(f(\theta _{0,\infty }(\bot _{D_0})))\\
v_{n+1} & \triangleq & \theta _{\infty ,n} \circ f \circ \theta _{n,\infty }
\end {array}