\begin {array}{lcl} \llbracket \mathsf {nat} \rrbracket &=& \mathbb {N}_\bot \\ \llbracket \tau _1 \rightarrow \tau _2 \rrbracket &=& \llbracket \tau _1 \rrbracket \twoheadrightarrow \llbracket \tau _2 \rrbracket \end {array}

For \Gamma \vdash e : \tau , we have \llbracket e \rrbracket _\Gamma : \llbracket \tau \rrbracket defined as follows: \begin {array}{lcl} \llbracket n \rrbracket _\Gamma (\vec {z}) & =& n\\ \llbracket x \rrbracket _\Gamma (\vec {z}) & = & z_j\ \text {where}\ j\ \text {is largest}\ j\ \text {s.t.}\ x = x_j \\ \llbracket \lambda x : \tau _1.\ e \rrbracket _\Gamma (\vec {z}) & = & (\boldsymbol {\lambda } v \in \llbracket \tau _1 \rrbracket .\ \llbracket e\rrbracket _{\Gamma , x : \tau _1}(\vec {z}, v))\\ \llbracket e_1\ e_2 \rrbracket _\Gamma (\vec {z}) & = & \llbracket e_1 \rrbracket _\Gamma (\vec {z})(\llbracket e_2 \rrbracket _\Gamma (\vec {z}))\\ \llbracket \mathsf {succ} \rrbracket _\Gamma (\vec {z}) & = & (\boldsymbol {\lambda } v \in \mathbb {N}_\bot .\ v + 1)\\ \llbracket \mathsf {pred} \rrbracket _\Gamma (\vec {z}) & = & (\boldsymbol {\lambda } v \in \mathbb {N}_\bot .\ v - 1)\\ \llbracket \mathsf {ifz}\ e_1\ \mathsf {then}\ e_2\ \mathsf {else}\ e_3 \rrbracket _\Gamma (\vec {z}) & = & \begin {cases} \llbracket e_2 \rrbracket _\Gamma (\vec {z}) & \text {if}\ \llbracket e_1 \rrbracket _\Gamma (\vec {z}) > 0 \\ \llbracket e_3 \rrbracket _\Gamma (\vec {z}) & \text {if}\ \llbracket e_1 \rrbracket _\Gamma (\vec {z}) = 0 \\ \bot & \text {if}\ \llbracket e_1 \rrbracket _\Gamma (\vec {z}) = \bot \end {cases}\\ \llbracket \mathsf {fix}\ x : \tau .\ e \rrbracket _\Gamma (\vec {z}) &= & \mathbf {fix}(\boldsymbol {\lambda } v \in \llbracket \tau \rrbracket .\ \llbracket e\rrbracket _{\Gamma , x : \tau }(\vec {z}, v)) \end {array} In the above definitions a boldface lambda \boldsymbol {\lambda } is used for an anonymous continuous function — boldface to distinguish it from the lambda in the syntax of PCF. Verifying that these functions are indeed continuous is straightforward, but is necessary to justify the use of the \mathbf {fix} operator.