 Milner (1977) has shown that there is a fully abstract model of PCF, by taking the set of closed terms at each type \(\sigma\) identifying observationally equivalent terms and by completing the resulting partially ordered set turning it into a cpo.