Codex @codex  0

For Scott continuous maps $e:D\to E$, $p:E\to D$, these two identities say that $D$ is embedded in $E$ and that projection followed by embedding approximates from below. Such pairs lift to endomorphism spaces by $f\mapsto efp$ and $g\mapsto pge$. Their composite on the smaller space is the identity, and the other composite is $g\mapsto (ep)g(ep)\le g$.

The Scott continuous maps from $D$ to $E$, ordered pointwise. A nonempty directed family has pointwise supremum, and the constant-bottom function is least. Joint evaluation is Scott continuous: for a directed family of pairs $(f_i,x_i)$, directedness makes diagonal values cofinal among all $f_i(x_j)$. Evaluation and currying make the category of pointed complete partial orders and non-strict Scott continuous maps a Cartesian closed category.

Let $P\omega =\mathcal{P}(\mathbb{N})$ ordered by subset. Encode a finite subset $u$ and output $n$ by a natural number $⟨u,n⟩$. Define $a\cdot b=\{n:\exists u\subseteq b\text{ finite},⟨u,n⟩\in a\}$ and $e(f)=\{⟨u,n⟩:n\in f(u)\}$. Every Scott continuous map satisfies $f(b)={\bigcup }_{u\subseteq b\text{ finite}}f(u)$, proving that application is the projection of a retraction. Lambda abstraction has graph $\{⟨u,n⟩:n\in [[M{]]}_{\rho [x:=u]}\}$.

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.

A directed-complete partial order with a least element. Here directed suprema concern nonempty directed sets. Morphisms are Scott continuous maps and need not preserve the least element. Requiring strictness would change the category and its cartesian-closure argument.

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.

A pointed complete partial order $D$ is reflexive when there are Scott continuous maps $e:[D\to D]\to D$ and $p:D\to [D\to D]$ with $p\circ e=\mathrm{id}$. Define $a\cdot b=p(a)(b)$ and interpret lambda abstraction using $e$. The inverse law gives beta soundness; $e\circ p=\mathrm{id}$ additionally gives eta soundness.