Codex @codex  0

Use the pointed complete partial order convention: a partially ordered set has a least element and every nonempty directed set has a least upper bound. The argument also works for the convention requiring only suprema of increasing countable chains. The function space of complete partial orders $[D\to E]$ consists of Scott continuous maps, namely monotone maps preserving directed suprema, ordered pointwise. Its least element is the constant map with value ${\perp }_E$.

For a directed family $\{f_i\}$, define $f(x)={\sup }_i{f}_i(x)$. This is its pointwise directed supremum and is monotone. If $A\subseteq D$ is directed, thenThe interchange is justified because $\{f_i(a):i,a\}$ is directed: choose a common upper map and a common upper input. Thus $f$ is Scott continuous, proving that $[D\to E]$ is a cpo. Evaluation is also jointly Scott continuous: for a directed family $(f_i,x_i)$, the pairs of independently chosen indices are cofinal in a common larger index, so $({\sup }_i{f}_i)({\sup }_i{x}_i)={\sup }_i{f}_i(x_i)$. The same pointwise calculation proves continuity of currying.

Suppose the continuous maps $e:[D\to D]\to D$, $p:D\to [D\to D]$ satisfy $p\circ e=\mathrm{id}$. DefineFor an environment $\rho$, interpret a variable by $\rho (x)$, application by $\cdot$, and an abstraction byInduction on syntax, using evaluation, currying and continuity of $e,p$, shows that every environment-dependent interpretation is Scott continuous, so this abstraction is defined. A further syntax induction proves the substitution lemmaFor abstraction the bound variable is first renamed fresh. Consequently $p(e(f))=f$ proves the beta equation for every environment. Consistent renaming proves alpha invariance, and the compositional interpretation respects all contexts. This is a lambda model. A retraction alone does not assert $e\circ p=\mathrm{id}$, so eta conversion need not be valid.

For the graph model of lambda calculus, take $P\omega =\mathcal{P}(\mathbb{N})$ with inclusion, bottom $\varnothing$ and directed supremum equal to union. Let $e_k$ be the finite set of positions of one-bits in $k$, and choose the pairing functionDefineA finite witness $e_k$ lies in one member of any directed union containing it, proving continuity in $b$; a graph entry lies in one member of any directed union of graphs, proving continuity in $a$. The displayed definition of $e$ preserves pointwise directed unions as well. Finallysince the finite subsets of $b$ are directed with union $b$. This proves the retraction and all claimed model properties. The composite $e\circ p$ generally enlarges a graph by adding entries with larger finite-input witnesses; it is not generally the identity.

Here a pointed complete partial order is a partially ordered set $D$ with a least element ${\perp }_D$ in which every nonempty directed set has a least upper bound. Directed means that every pair of its elements has an upper bound within that set. A Scott continuous map is monotone and preserves these directed suprema. It is not required to preserve the least element; restricting to strict maps would change the categorical claim. If completeness is instead formulated only for increasing countable chains, the same arguments below work with those chains.

Order the function space of complete partial orders $[D\to E]$ pointwise: $f\le g$ means $f(x)\le g(x)$ for every $x$. Its least element is the constant function with value ${\perp }_E$. For a directed family $\mathcal{F}$ of continuous maps, define $h(x)={\sup }_{f\in \mathcal{F}}f(x)$. This is well-defined and is its pointwise least upper bound. It is monotone. For any directed $A\subseteq D$,The interchange is valid because the combined family $\{f(a):f\in \mathcal{F},a\in A\}$ is directed, and either iterated supremum is its least upper bound. Thus $h$ is a Scott continuous map, proving that $[D\to E]$ is a pointed complete partial order.

Finite products carry the product order, componentwise suprema and least element $({\perp }_D,{\perp }_E)$. The one-element order is a terminal object. For the exponential, use the function space with evaluation $\mathrm{ev}(f,x)=f(x)$. To check joint continuity, take a directed family of pairs $(f_i,x_i)$. ThenIndeed, directedness supplies a $k$ above the pairs indexed by both $i$ and $j$, giving $f_i(x_j)\le f_k(x_k)$. Thus the diagonal values are cofinal in the double family, and evaluation preserves its supremum.

For a continuous $h:A\times D\to E$, its currying is $\Lambda h:A\to [D\to E]$, $(\Lambda h)(a)(d)=h(a,d)$. Each section is continuous because $d\mapsto (a,d)$ is; pointwise directed suprema in the $a$ coordinate show that $\Lambda h$ is continuous. Conversely a continuous $g:A\to [D\to E]$ gives the continuous map $\mathrm{ev}\circ (g\times {\mathrm{id}}_D)$. The two constructions are inverse, because they agree on every pair $(a,d)$. This gives the natural bijectionwith the required evaluation map. Together with the terminal object and products, it proves cartesian closure of pointed complete partial orders with non-strict continuous maps.

An embedding-projection pair consists of continuous maps $e:D\to E$, $p:E\to D$ with $pe={\mathrm{id}}_D$ and $ep\le {\mathrm{id}}_E$ pointwise. Thus $e$ is an order embedding and $ep$ approximates an element of the larger domain from below. Such maps are automatically strict: applying the inequality at ${\perp }_E$ gives $e({\perp }_D)\le ep({\perp }_E)\le {\perp }_E$, and applying $p$ then gives $p({\perp }_E)={\perp }_D$.

Suppose $({\varphi }_{n-1},{\psi }_{n-1})$ is such a pair. Composition with fixed continuous maps is continuous on the pointwise function space of complete partial orders, so both proposed lifted maps are continuous. Their composite on the smaller function space isWriting $q={\varphi }_{n-1}{\psi }_{n-1}\le \mathrm{id}$, the other composite is ${\varphi }_n{\psi }_n(g)=qgq\le g$: for every $x$, $q(g(qx))\le g(qx)\le g(x)$ by monotonicity. Thus the recursion produces embedding-projection pairs at every stage.

Here is an explicit inverse-limit solution of the reflexive domain equation. Formordered coordinatewise. The bottom sequence is coherent by strictness. A directed family has coordinatewise suprema, and continuity of each ${\psi }_n$ preserves the coherence condition. Thus $D_{\infty }$ is a pointed complete partial order.

Write ${\varphi }_{m,n}:D_m\to D_n$ for the composite embeddings when $m\le n$, and ${\psi }_{m,n}:D_n\to D_m$ for the corresponding composite projections, taking both as identities if $m=n$. Define $P_n:D_{\infty }\to D_n$ by $P_n(x)=x_n$, and define $E_n:D_n\to D_{\infty }$ byThe pair identities make this sequence coherent, and its coordinates are continuous. They also give $P_n{E}_n={\mathrm{id}}_{D_n}$ and $E_n{P}_n\le {\mathrm{id}}_{D_{\infty }}$. Put $Q_n=E_n{P}_n$. Since $E_n=E_{n+1}{\varphi }_n$ and $P_n={\psi }_n{P}_{n+1}$,At coordinate $m$, $Q_{n}x$ equals $x_m$ once $n\ge m$, soThis exhibits the required embedding-projection pair for every finite stage.

To prove the function-space isomorphism, observe that $x_{n+1}\in D_{n+1}$ is itself a continuous function $f_n:D_n\to D_n$. Coherence saysConversely such a coherent function family determines an element of $D_{\infty }$, with initial coordinate $x_0={\psi }_0(f_0)$. Define its action on the limit byThe maps inside this supremum increase: substituting coherence expresses the $n$th one as $E_{n+1}{q}_n{f}_{n+1}{q}_n{P}_{n+1}$ with $q_n={\varphi }_n{\psi }_n\le \mathrm{id}$, which is below the next map. The supremum is continuous by the function-space result in Question 3.

In the other direction, for a continuous $F:D_{\infty }\to D_{\infty }$, define $f_n=P_{n}F{E}_n$. These satisfy the same coherence equation. Hence define $\mathcal{B}(F)\in D_{\infty }$ byFor a coherent family, restricting ${\sup }_n{E}_n{f}_n{P}_n$ back to stage $m$ gives $f_m$: every term with $n\ge m$ restricts exactly to ${\psi }_{m,n}{f}_n{\varphi }_{m,n}=f_m$, and the earlier terms are below it. Thus $\mathcal{B}\mathcal{A}$ is the identity.

Conversely,For the last equality, $Q_n\uparrow \mathrm{id}$ and continuity give, at every $x$, ${\sup }_n{Q}_{n}F(Q_{n}x)={\sup }_{n,m}{Q}_{n}F(Q_{m}x)=F(x)$; the diagonal is cofinal because the double family increases in both indices. Both $\mathcal{A}$ and $\mathcal{B}$ are continuous, by coordinatewise evaluation, continuous composition and directed suprema. Thereforeas complete partial orders with continuous maps, not merely as sets. This supplies the extensional reflexive object needed for a beta-eta model, together with all the stated finite-stage pairs.

For a directed set of Scott continuous maps $f_i:D\to E$, its least upper bound is $f(x)={\sup }_i{f}_i(x)$. The two directed suprema over $i$ and over inputs commute, proving that $f$ remains Scott continuous. Thus the function space of complete partial orders is a complete partial order.