= Solution
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 $\bot_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, then
$$
f(\sup A)=\sup_i f_i(\sup A)=\sup_i\sup_{a\in A}f_i(a)=\sup_{a\in A}\sup_i f_i(a)=\sup_{a\in A}f(a).
$$
The 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 \b[$[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}$. Define
$$
\boxed{a\cdot b=p(a)(b).}
$$
For an environment $\rho$, interpret a variable by $\rho(x)$, application by $\cdot$, and an abstraction by
$$
\llbracket\lambda x.M\rrbracket_\rho=e\bigl(d\mapsto\llbracket M\rrbracket_{\rho[x:=d]}\bigr).
$$
Induction 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 lemma
$$
\llbracket M[x:=N]\rrbracket_\rho=\llbracket M\rrbracket_{\rho[x:=\llbracket N\rrbracket_\rho]}.
$$
For 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 function>
$$
\langle k,n\rangle=\frac{(k+n)(k+n+1)}2+n.
$$
Define
$$
p(a)(b)=a\cdot b=\{n:\exists k\;(e_k\subseteq b\ \text{and}\ \langle k,n\rangle\in a)\},\qquad e(f)=\{\langle k,n\rangle:n\in f(e_k)\}.
$$
A 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. Finally
$$
p(e(f))(b)=\bigcup_{e_k\subseteq b}f(e_k)=f(b),
$$
since 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.
Back to article page
