 A model of PCF is an interpretation that satisfies the expected identities between terms of the same type. We shall omit the details of the general characterization of models of PCF, for which the reader is referred to Ong (1995: sec. 3.2) and Berry, Curien, &amp; Lévy (1985: sec. 4), but just to point out an example of what must be taken into account when such a generality is needed, in order to admit interpretations where the elements at function types are not, strictly speaking, functions, we have to assume a family of application operations   \[\cdot_{\sigma\tau}: D^{\sigma \to \tau} \times D^\sigma \to D^\tau\]   so that, if \(B \vdash e_1 : \sigma \to \tau\) and \(B \vdash e_2 ; \sigma\), \({\lll e_1e_2\rll \rho} = {\lll e_1\rll \rho} \cdot_{\sigma\tau} {\lll e_2\rll \rho} \in {{{D}^{\tau}}}\). A model is order-extensional if, for all elements \(f,g \in {{{D}^{\sigma \to \tau}}}\), \(f \sqsubseteq g\) if and only if \(f \cdot x \sqsubseteq g \cdot x\) for all \(x \in {{{D}^{\sigma}}}\). A model is extensional if, for all elements \(f,g \in {{{D}^{\sigma \to \tau}}}\), \(f = g\) if and only if \(f \cdot x = g \cdot x\) for all \(x \in {{{D}^{\sigma}}}\). An element \(d \in D^\sigma\) of a model is definable is there is a closed terms \(e:\sigma\) such that \(d = {\lll e\rll }\).