Programming Computable Functions

The data types of PCF are inductively defined as • nat is a type • For types σ and τ, there is a function type σ → τ A context is a list of pairs x : σ, where x is a variable name and σ is a type, such that no variable name is duplicated. One then defines typing judgments of terms-in-context in the usual way for the following syntactical constructs: • Variables (if x : σ is part of a context Γ, then Γ ⊢ x : σ) • Application (of a term of type σ → τ to a term of type σ) • λ-abstraction • The Y fixed point combinator (making terms of type σ out of terms of type σ → σ) • The successor (succ) and predecessor (pred) operations on nat and the constant 0 • The conditional if with the typing rule: : \frac{ \Gamma \; \vdash \; t \; : \textbf{nat} , \quad \quad \Gamma \; \vdash \; s_0 \; : \sigma , \quad \quad \Gamma \; \vdash \; s_1 \; : \sigma } { \Gamma \; \vdash \; \textbf{if}(t,s_0,s_1) \; : \sigma } : (nats will be interpreted as booleans here with a convention like zero denoting truth, and any other number denoting falsity) ==Semantics==

Denotational semantics A relatively straightforward semantics for the language is the Scott model. In this model, • Types are interpreted as certain domains. • [\![ \textbf{nat} ]\!] := \mathbb{N}_{\bot} (the natural numbers with a bottom element adjoined, with the flat ordering) • [\![ \sigma \to \tau \, ]\!] is interpreted as the domain of Scott-continuous functions from [\![\sigma]\!] \, to [\![\tau]\!] \,, with the pointwise ordering. • A context x_1 : \sigma_1, \; \dots, \; x_n : \sigma_n is interpreted as the product [\![\sigma_1]\!] \times \; \dots \; \times [\![\sigma_n]\!] • Terms in context \Gamma \; \vdash \; x \; : \; \sigma are interpreted as continuous functions [\![\Gamma]\!] \; \to \; [\![\sigma]\!] • Variable terms are interpreted as projections • Lambda abstraction and application are interpreted by making use of the cartesian closed structure of the category of domains and continuous functions • Y is interpreted by taking the least fixed point of the argument This model is not fully abstract for PCF; but it is fully abstract for the language obtained by adding a parallel or operator to PCF. == Notes ==