Natural non-dcpo Domains and f-Spaces

Vladimir Sazonov

Department of Computer Science, the University of Liverpool, 
Liverpool L69 3BX, U.K., v.sazonov@csc.liv.ac.uk


Let Q be the fully abstract (universal) model of hereditarily-
sequential finite type functionals for PCF (constructed via game 
semantics by S. Abramsky, R. Jagadeesan, and P.Malacaria; 
J. M. E. Hyland and C.-H. L. Ong; H. Nickau, and also recently 
constructed again by the author inductively, level-by-level). 
This model, unlike the old fully abstract continuous directed 
complete partially ordered (dcpo) model of Robin Milner (1977), 
is universal in the sense that it contains definable universal 
(surjective) functionals U_T:(N -> N) -> T for each type T. As 
Dag Normann has recently shown, Q is a non-dcpo model -- in fact, 
non-omega-complete -- and therefore not continuous in the 
traditional terminology. Non-omega-completeness holds also for 
the (unique) fully abstract universal model W for PCF^+ = PCF + 
parallel IF and should surely hold for a wider class of similar 
models. Any "positive" domain theoretic properties of these 
non-dcpo models were unknown. 

Here we will present a general non-dcpo domain theoretic approach 
to such kind of models. So called "natural" domains are introduced 
which, although being in general non-dcpos, allow considering 
"naturally" continuous functions with respect to existing directed 
"pointwise", or "natural" least upper bounds (lubs). In particular, 
the above non-dcpo modes Q and W are naturally continuous in this 
sense and satisfy the following properties. Similarly to the 
ordinary dcpo-domains, naturally omega-algebraic and naturally 
bounded complete natural non-dcpo domains can be considered (again, 
all of this with respect to existing directed natural lubs -- not 
each lub being natural). This means roughly that the set of 
naturally finite elements of such a domain is sufficiently rich. 
Naturally finite elements are defined exactly as finite (algebraic) 
ones in dcpos, but with respect to existing natural directed least 
upper bounds. It is shown that the general class of natural 
non-dcpo domains satisfying the above (natural) algebraicity and 
bounded completeness properties is equivalent to Yuri Ershov's 
general (not necessarily complete) f-spaces. Recall that complete 
f_0-spaces are equivalent to Dana Scott's dcpo domains (satisfying 
the ordinary algebraicity and bounded completeness properties). 

The point of these considerations and the value of the general 
concept of natural non-dcpo domain is that the above models Q for 
PCF and W for PCF^+ immediately appear as natural non-dcpo models 
rather than as explicit non-dcpo f-space models -- the a posteriori 
fact. The natural continuity, natural algebraicity, etc. properties 
of these models have non-trivial proof heavily using the author's 
old theory of sequential computational strategies. The proof is 
based on a particular, "pointwise" version of typed "natural" 
non-dcpo lambda models (to appear in the Journal LMCS).

Keywords: domain theory, dcpo and non-dcpo domains, f-spaces, 
Scott domains, algebraic, PCF, full abstraction, sequentiality