It is well-known that the only fully abstract order-extensional model of PCF is isomorphic to the syntax itself; this is an old result due to [Milner 1977].
However, there are many tricks one can play to "circumvent" this theorem.
Game semantics can be used to construct an equivalent presentation of this syntax, in which the denotations of terms are given as strategies structured in a question-answer fashion.
This leads an intensional model, which requires a further "observational" quotient to be a model of observational equivalence of PCF.
See game semantic models of PCF for more details.
Another way to construct a fully abstract model of PCF is to use [Kripke logical relations], an approach due to [O'Hearn and Riecke 1995].
This approach consists of starting with the usual [Scott model of PCF], and using Kripke logical relations to "pick out" the "hereditarily sequential elements" of the model. This does not require quotienting, as the "picking out" starts at the very bottom of the type hierarchy.
Because this model is order-extensional, [O'Hearn and Riecke 1995] point out that their construction is isomorphic to the syntactic model of [Milner 1997].
This approach
There are also other ways to construct "models" of PCF. These are not necessarily denotational in the traditional sense (viz. mathematical objects whose equality coincides exactly with the observational equivalence). Rather, they take the form of low-level operational descriptions, such as labelled transition systems, and are equipped with some notion of bisimulation.
Fully abstract models based on applicative bisimulation can be found in [Abramsky 1990], [Gordon 1994], and [Howe 1996].
Milner, Robin. 1977. ‘Fully Abstract Models of Typed λ-Calculi’. Theoretical Computer Science 4 (1): 1–22. https://doi.org/10.1016/0304-3975(77)90053-6.
@article{milner_1977,
title = {Fully abstract models of typed λ-calculi},
volume = {4},
issn = {03043975},
doi = {10.1016/0304-3975(77)90053-6},
number = {1},
journal = {Theoretical Computer Science},
author = {Milner, Robin},
year = {1977},
pages = {1--22}
}
O’Hearn, Peter W., and J.G. Riecke. 1995. ‘Kripke Logical Relations and PCF’. Information and Computation 120 (1): 107–16. https://doi.org/10.1006/inco.1995.1103.
@article{ohearn_1995,
title = {Kripke {Logical} {Relations} and {PCF}},
volume = {120},
doi = {10.1006/inco.1995.1103},
number = {1},
journal = {Information and Computation},
author = {O'Hearn, Peter W. and Riecke, J.G.},
year = {1995},
pages = {107--116}
}
Abramsky, Samson. 1990. ‘The Lazy Lambda Calculus’. In Research Topics in Functional Programming, 65–117. Addison Wesley. [pdf]
@incollection{abramsky_1990,
title = {The {Lazy} {Lambda} {Calculus}},
url = {https://www.cs.ox.ac.uk/files/293/lazy.pdf},
booktitle = {Research {Topics} in {Functional} {Programming}},
publisher = {Addison Wesley},
author = {Abramsky, Samson},
year = {1990},
pages = {65--117}
}
Gordon, Andrew D. 1994. Functional Programming and Input/Output. Distinguished Dissertations in Computer Science. Cambridge University Press. [pdf]
@book{gordon_1994,
series = {Distinguished {Dissertations} in {Computer} {Science}},
title = {Functional programming and input/output},
url = {https://www.microsoft.com/en-us/research/publication/functional-programming-input-output/},
publisher = {Cambridge University Press},
author = {Gordon, Andrew D.},
year = {1994}
}
Howe, Douglas J. 1996. ‘Proving Congruence of Bisimulation in Functional Programming Languages’. Information and Computation 124 (2): 103–12. https://doi.org/10.1006/inco.1996.0008. [pdf]
@article{howe_1996,
title = {Proving {Congruence} of {Bisimulation} in {Functional} {Programming} {Languages}},
volume = {124},
doi = {10.1006/inco.1996.0008},
number = {2},
journal = {Information and Computation},
author = {Howe, Douglas J.},
year = {1996},
pages = {103--112}
}