A metric model of PCF

We introduce a computationally adequate metric model of PCF, based on the fact that the category of non-expansive maps of complete bounded ultrametric spaces is cartesian closed. The model captures certain temporal aspects of higher-type computation and contains both extensional and intensional functions. We show that Scott's model arises as its extensional collapse. The intensional aspects of the metric model are illustrated via a Godel-number-free version of Kleene's T -predicate. Keywords: Simply typed lambda-calculus, higher-type recursion theory, metric semantics. MSC: 03B40, 03D65, 68Q55. 1 Introduction Scott's model of PCF is based on the introduction of bottom elements in the interpretation of ground types [14]. Conceptually, bottom stands for absence of information. This is made mathematically precise via the information order. Computationally, bottom stands for non-termination. The precise formulation of this statement is referred to as computational adequacy : A PCF progr..