The language for Programming Computable Functions (PCF) is a variant of typed \lambda -calculus with minimal extensions to be Turing-complete. \begin {array}{lcl} e & \Coloneqq & n \mid x \mid \lambda x : \tau .\ e \mid e_1\ e_2\mid \mathsf {succ} \mid \mathsf {pred} \mid \mathsf {ifz}\ e_1\ \mathsf {then}\ e_2\ \mathsf {else}\ e_3 \mid \mathsf {fix}\ x : \tau .\ e \\ \tau & \Coloneqq & \mathsf {nat} \mid \tau _1 \rightarrow \tau _2 \end {array}

\dfrac {n \in \mathbb {N}}{\Gamma \vdash n : \mathsf {nat}}\quad \dfrac {x : \tau \in \Gamma }{\Gamma \vdash x : \tau }\quad \dfrac {\Gamma , x : \tau _1 \vdash e : \tau _2 }{ \Gamma \vdash \lambda x : \tau _1.\ e : \tau _1 \rightarrow \tau _2}\quad \dfrac {\Gamma \vdash e_1 : \tau _1 \rightarrow \tau _2 \quad \Gamma \vdash e_2 : \tau _1}{\Gamma \vdash e_1\ e_2 : \tau _2}\\[2em] \dfrac { }{ \Gamma \vdash \mathsf {succ} : \mathsf {nat} \rightarrow \mathsf {nat}}\quad \dfrac { }{ \Gamma \vdash \mathsf {pred} : \mathsf {nat} \rightarrow \mathsf {nat}}\quad \dfrac { \Gamma \vdash e_1 : \mathsf {nat} \quad \Gamma \vdash e_2 : \tau \quad \Gamma \vdash e_3 : \tau }{ \Gamma \vdash \mathsf {ifz}\ e_1\ \mathsf {then}\ e_2\ \mathsf {else}\ e_3 : \tau }\quad \dfrac { \Gamma , x : \tau \vdash e : \tau }{\Gamma \vdash \mathsf {fix}\ x : \tau .\ e : \tau }

Because PCF is typed, we shall assign denotations only to well-typed expressions. The range of our denotation function for expressions is determined by the type of its input expression. That is, the denotation of a type \tau is the cpo whose elements will be the denotations of expressions of type \tau . The denotation of the type \mathsf {nat}, then, is merely the flat domain of the natural numbers \mathbb {N}_\bot : \llbracket \mathsf {nat} \rrbracket = \mathbb {N}_\bot And, the denotation of the function type is the domain of continuous functions on cpos: \llbracket \tau _1 \rightarrow \tau _2 \rrbracket = \llbracket \tau _1 \rrbracket \twoheadrightarrow \llbracket \tau _2 \rrbracket A closed term e : \tau with no free variables denotes an element of \llbracket \tau \rrbracket , so we might be tempted to define our denotation function for expressions e : \tau like so: \llbracket e \rrbracket : \llbracket \tau \rrbracket However, if e : \tau involves free variables from our context \Gamma , the valuation of e will depend on the values assigned to all the variables. Thus, the denotation of a typed expression \Gamma \vdash e : \tau is defined instead as a continuous function: \llbracket e \rrbracket _\Gamma : \llbracket \Gamma \rrbracket \twoheadrightarrow \llbracket \tau \rrbracket where the meaning of a context \Gamma = (x_0 : \tau _0, x_1 : \tau _1,\dots , x_n : \tau _n) will be a a big n-tuple of the values assigned to each variable: \llbracket \Gamma \rrbracket = \llbracket \tau _0 \rrbracket \times \llbracket \tau _1 \rrbracket \times \cdots \times \llbracket \tau _n \rrbracket

Given an n-tuple, i.e. elements of the n-ary product X_0 \times X_1 \times X_2 \times \dots \times X_n, we typically denote the entire n-tuple as in vector notation: \vec {x} : X_0 \times X_1 \times X_2 \times \dots \times X_n And individual elements of the tuple are accessed with numeric subscripts: x_0 : X_0 \quad x_2 : X_2 \quad \cdots

We shall extend the syntax of PCF with a new type former, \tau _1 \times \tau _2 and three expression-level constructs for constructing and deconstructing pairs: \begin {array}{lcl} e & \Coloneqq & \cdots \mid (e_1,e_2) \mid \mathsf {fst}\ e \mid \mathsf {snd}\ e \\ \tau & \Coloneqq & \cdots \mid \tau _1 \times \tau _2 \end {array} Adding to our typing rules similarly: \dfrac {\Gamma \vdash e_1 : \tau _1 \quad e_2 : \tau _2}{(e_1,e_2) : \tau _1 \times \tau _2}\\[2em] \dfrac {\Gamma \vdash e : \tau _1 \times \tau _2}{\Gamma \vdash \mathsf {fst}\ e : \tau _1}\quad \dfrac {\Gamma \vdash e : \tau _1 \times \tau _2}{\Gamma \vdash \mathsf {snd}\ e : \tau _2} To extend our semantics, we make the product type \tau _1 \times \tau _2 denote the product cpo \llbracket \tau _1 \rrbracket \times \llbracket \tau _2 \rrbracket , and our expression semantics are expressed straightforwardly using our projection and split operations for products: \begin {array}{lcl} \llbracket (e_1, e_2) \rrbracket _\Gamma &=& \langle \llbracket e_1 \rrbracket _\Gamma , \llbracket e_2 \rrbracket _\Gamma \rangle \\ \llbracket \mathsf {fst}\ e \rrbracket _\Gamma & = & \pi _0 \circ \llbracket e \rrbracket _\Gamma \\ \llbracket \mathsf {snd}\ e \rrbracket _\Gamma & = & \pi _1 \circ \llbracket e \rrbracket _\Gamma \\ \end {array}

We shall extend the syntax of PCF with a new type former, \tau _1 + \tau _2 and three expression-level constructs for constructing and deconstructing sums: \begin {array}{lcl} e & \Coloneqq & \cdots \mid \mathsf {inl}\ e \mid \mathsf {inr}\ e \mid \mathsf {case}\ e_0\ \mathsf {of}\ \mathsf {inl}\ x \rightarrow e_1 ; \mathsf {inr}\ y \rightarrow e_2 \\ \tau & \Coloneqq & \cdots \mid \tau _1 + \tau _2 \end {array} Adding to our typing rules similarly: \dfrac {\Gamma \vdash e : \tau _1}{\Gamma \vdash \mathsf {inl}\ e : \tau _1 + \tau _2}\quad \dfrac {\Gamma \vdash e : \tau _2}{\Gamma \vdash \mathsf {inr}\ e : \tau _1 + \tau _2}\\[2em] \dfrac {\Gamma \vdash e_0 : \tau _1 + \tau _2 \quad \Gamma , x : \tau _1 \vdash e_1 : \tau \quad \Gamma , y : \tau _2 \vdash e_2 : \tau }{ \Gamma \vdash \mathsf {case}\ e_0\ \mathsf {of}\ \mathsf {inl}\ x \rightarrow e_1 ; \mathsf {inr}\ y \rightarrow e_2 : \tau } To extend our semantics, we make the sum type \tau _1 + \tau _2 denote the sum cpo \llbracket \tau _1 \rrbracket + \llbracket \tau _2 \rrbracket , and our expression semantics are expressed using our primitive functions for sums. \begin {array}{lcl} \llbracket \mathsf {inl}\ e \rrbracket _\Gamma & = & \mathit {inl} \circ \llbracket e \rrbracket _\Gamma \\ \llbracket \mathsf {inr}\ e \rrbracket _\Gamma & = & \mathit {inr} \circ \llbracket e \rrbracket _\Gamma \end {array} \begin {array}{l}\llbracket \mathsf {case}\ e_0\ \mathsf {of}\ \mathsf {inl}\ x \rightarrow e_1 ; \mathsf {inr}\ y \rightarrow e_2 \rrbracket _\Gamma (\vec {z}) \\ \quad = [ \boldsymbol {\lambda }v. \llbracket e_1 \rrbracket _{\Gamma ,x:\tau _1}(\vec {z},v), \boldsymbol {\lambda }v. \llbracket e_2 \rrbracket _{\Gamma ,y:\tau _2}(\vec {z},v)] (\llbracket e_0 \rrbracket _\Gamma (\vec {z}))\end {array}