Graph model of lambda calculus (source code)

= Graph model of lambda calculus
{title2=$P\omega$}

= Pomega model
{c}
{synonym}

Let $P\omega=\mathcal P(\mathbb N)$ ordered by <subset>. Encode a finite subset $u$ and output $n$ by a natural number $\langle u,n\rangle$. Define $a\cdot b=\{n:\exists u\subseteq b\text{ finite},\ \langle u,n\rangle\in a\}$ and $e(f)=\{\langle u,n\rangle: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 $\{\langle u,n\rangle:n\in\llbracket M\rrbracket_{\rho[x:=u]}\}$.