Models of PCF

There are many ways to construct denotational models of PCF.

The original model presented by Scott and Plotkin used domain-theoretic techniques to interpret recursion. The construction predates both of them, and is essentially due to Platek.

However, there are many models of PCF with a non-domain-theoretic flavour. However, because of the presence of recursion, such models invariably contain of some kind of domain-theoretic structure somewhere - even if that only consists of least upper bound of rational chains.

The following styles of model have been used:

domain-theoretic models (and variations)
coherence spaces
relational models
models based on game semantics

Categorical description

The most general description of a model of PCF can be found by straightforwardly translating the typing rules to category theory

In short, it consists of a cartesian closed category that supports a bunch of constants of the appropriate type, satisfying the equational theory that is induced by the operational semantics.

An explicit description of that may be found in Hyland and Ong 2000.

The domain-theoretic model

Please expand.

References

Hyland, J.M.E., and C.-H.L. Ong. 2000. “On Full Abstraction for PCF: I, II, and III.” Information and Computation 163 (2): 285–408. https://doi.org/10.1006/inco.2000.2917.

@article{Hyland2000,
author = {Hyland, J.M.E. and Ong, C.-H.L.},
doi = {10.1006/inco.2000.2917},
issn = {08905401},
journal = {Information and Computation},
number = {2},
pages = {285--408},
title = {On Full Abstraction for PCF: I, II, and III},
url = {https://linkinghub.elsevier.com/retrieve/pii/S0890540100929171},
volume = {163},
year = {2000}
}