Type-dependent denotations [dt-003O]

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