  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
simple extension of PCF. We then introduce an intrinsic preorder on strategies,
and show that it satisfies some striking properties, such that the intrinsic
preorder on function types coincides with the pointwise preorder. We then
obtain an order-extensional fully abstract model of PCF by quotienting the
intensional model by the intrinsic preorder. This is the first
syntax-independent description of the fully abstract model for PCF. (Hyland and
Ong have obtained very similar results by a somewhat different route,
independently and at the same time).
  We then consider the effective version of our model, and prove a Universality
Theorem: every element of the effective extensional model is definable in PCF.
Equivalently, every recursive strategy is definable up to observational
equivalence.
