Complete Partial Orders

Abstract

In Chapter 3.1 we have defined constructivity and computability on the sets P_ω, IB_o, and ℂ_o explicitly (Def. 3.1.3, 3.1.8, 3.1.10). The three definitions are very similar. They are special cases of a general theory, the theory of complete partial orders (cpo’s). Complete partial orders are used as domains for the semantics (the denotational semantics) of programming languages. But independently of this application they are an interesting general model for studying Type 2 constructivity and computability. We shall not develop a general theory of cpo’s but essentially study a special class of cpo’s, the class of boundedly-complete algebraic cpo’s with countable basis. This chapter contains the topological framework. CPO’s and the continuous functions are defined. Algebraic cpo’s are introduced. For any algebraic cpo a topology can be defined such that order-continuity and topological continuity coincide. It is shown that the class of cpo’s is closed w.r.t. sum and product. The most remarkable property is that the space of the continuous functions between two cpo’s is a cpo again. The algebraic basises of the standard sum, product, and function space of b-complete algebraic cpo’s are defined explicitly. Finally the recursion theorem for cpo’s is proved. Constructivity and computability are investigated in the next two chapters.