CCC's of algebraic dcpo's

In this chapter, we provide a finer analysis of algebraicity. The central result – which was conjectured by Plotkin and was first proved in [Smy83a] – is that there exists a maximum cartesian closed full subcategory (full sub-CCC) of ω Acpo (the category of ω-algebraic cpo's). Jung has extended this result: he has characterized the maximal cartesian closed full subcategories of Acpo and Adcpo (and of ω Adcpo as well). In section 5.1, we define continuous dcpo's, which are dcpo's where approximations exist without being necessarily compact. Continuous lattices have been investigated in depth from a mathematical perspective [GHK + 80]. Our interest in continuous dcpo's arises from the fact that retracts of algebraic dcpo's are not algebraic in general, but are continuous. Much of the technical work involved in our quest of maximal full cartesian closed subcategories of (d)cpo's involves retracts. In section 5.2, we introduce two cartesian closed categories: the category of profinite dcpo's and the category of L-domains, both with continuous functions as morphisms. In section 5.3, we show that the algebraic L-domains and the bifinite domains form the two maximal cartesian closed full subcategories of Acpo , and derive Smyth's result for ω Acpo with little extra work. In section 5.4, we treat more sketchily the situation for Adcpo . The material of sections 5.3 and 5.4 is based on [Jun88]. In section 5.5, we show a technical result needed in section 5.3: a partial order is a dcpo if and only if all its well-founded subsets have a lub.