Full abstraction for PCF

An intensional model for the programming language PCF is described in which the types of PCF are interpreted by games and the terms by certain history -free strategies. This model is shown to capture definability in PCF. More precisely, every compact strategy in the model is definable in a certain si mple extension of PCF. We then introduce an intrinsic preorder on strategie s and show that it satisfies some striking properties such that the intrins ic preorder on function types coincides with the pointwise preorder. We the n obtain an order-extensional fully abstract model of PCF by quotienting th e intensional model by the intrinsic preorder. This is the first syntax-ind ependent description of the fully abstract model for PCF. (Hyland and Ong h ave obtained very similar results by a somewhat different route, independen tly and at the same time. ) We then consider the effective version of our model and prove a universalit y theorem: every element of the effective extensional model is definable in PCF. Equivalently, every recursive strategy is definable up to observation al equivalence. (C) 2000 Academic Press.