Approximation and function spaces
Jean Goubault-Larrecq · Cambridge University Press eBooks · 2013
In Section 4.2.2, we discussed how computer programs could be thought of as computing values x obtained as sup n ∈ℕ x n , where x n are values in a given dcpo, e.g., the dcpo of sets of formulae in the example of the automated theoremproving computer. A distinguishing feature of the approximants x n to x is that they are finite, and this particular relation between x n and x can be described in arbitrary posets by saying that x n is way-below x . The way-below relation ≪ is a fundamental notion, leading to so-called continuous and algebraic dcpos, and we define it and study it in Section 5.1. Beyond dcpos, the way-below relation will be instrumental in studying the lattice of open subsets of a topological space (Section 5.2). This will lead us to investigate the spaces whose lattice of open subsets is continuous, the so-called core-compact spaces. We shall see that the core-compact spaces are exactly the spaces X that are exponentiable, that is, such that we can define a topology on the space [ X → Y ] of continuous maps from X to an arbitrary space Y so that application and currification are themselves continuous (Section 5.3). These are basic requirements in giving semantics to higher-order programming languages, and desirable features in algebraic topology. The way-below relation The approximation , or way-below relation ≪ on a poset X is of fundamental importance in the study of dcpos.