We recapitulate the axiomatic foundations on which this book is based in Section 2.1. We then recall a few points about finiteness and countability in Section 2.2 and some basics of order theory in Section 2.3, and discuss the Axiom of Choice and some of its consequences in Section 2.4. These points will be needed often in the rest of this book. If you prefer to read about topology right away, and feel confident enough, please proceed directly to Chapter 3.

Foundations

We shall rest on ordinary set theory. While the latter has been synonymous with Zermelo–Fraenkel (ZF) set theory with the Axiom of Choice (ZFC) for some time, we shall use von Neumann–Gödel–Bernays (VBG) set theory instead (Mendelson, 1997).

There is not much difference between these theories: VBG is a conservative extension of ZFC. That VBG is an extension means that any theorem of ZFC is also a theorem of VBG. That it is conservative means that any theorem of VBG that one can express in the language of ZFC is also provable in ZFC.

The main difference between VBG and ZFC is that the former allows one to talk about collections that are too big to be sets. This is required, in all rigor, in the definition of (big) graphs and categories of Section 4.12. VBG allows us to talk about, say, the collection V of all sets, although V cannot itself be a set. This is the essence of Russell's paradox: assume there were a set V of all sets.

In Section 4.2.2, we discussed how computer programs could be thought of as computing values x obtained as supn∈ℕxn, where xn 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 xn to x is that they are finite, and this particular relation between xn and x can be described in arbitrary posets by saying that xn 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.

Purpose This book is an introduction to some of the basic concepts of topology, especially of non-Hausdorff topology. I will of course explain what it means (Definition 4.1.12). The important point is that traditional topology textbooks assume the Hausdorff separation condition from the very start, and contain very little information on non-Hausdorff spaces. But the latter are important already in algebraic geometry, and crucial in fields such as domain theory.

Conversely, domain theory (Abramsky and Jung, 1994; Gierz et al., 2003), which arose from logic and computer science, started as an outgrowth of theories of order. Progress in this domain rapidly required a lot of material on (non-Hausdorff) topologies.

After about 40 years of domain theory, one is forced to recognize that topology and domain theory have been beneficial to each other. I've already mentioned what domain theory owes to topology. Conversely, in several respects, domain theory, in a broad sense, is topology done right.

This book is an introduction to both fields, dealt with as one. This seems to fill a gap in the literature, while bringing them forth in a refreshing perspective.

Secondary purpose This book is self-contained. My main interest, though, as an author, was to produce a unique reference for the kind of results in topology and domain theory that I needed in research I started in 2004, on semantic models of mixed non-deterministic and probabilistic choice.

In Chapter 4, we mentioned a connection between topology and order, centered around the notion of specialization quasi-ordering. The connection between topology and order goes much beyond this. For any topological space X, O(X) is a poset, of a rather special kind, and we start by examining when a poset L is of this form for some space X. The posets that have this property are the spatial lattices, and Stone duality is a canonical way of retrieving the space X of points from the lattice L alone; see Section 8.1. Conversely, the spaces X of points obtained from spatial lattices are exactly the sober topological spaces, and any space can be completed to a sober space. This is explored in Section 8.2. The sober spaces have wonderful properties, and the single most important result about sober spaces is the Hofmann–Mislove Theorem, which we establish and whose consequences we state in Section 8.3. This is the starting point of a theory of correspondences between certain spaces and certain lattices: sober spaces and spatial lattices, but also sober locally compact spaces and continuous distributive complete lattices, or continuous dcpos with their Scott topology and completely distributive lattices notably. We then look at limits and colimits in Top, and how they are preserved or not by the sobrification functor in Section 8.4.

The inductive and the coinductive types are two important forms of recursive type. Inductive types correspond to least, or initial, solutions of certain type isomorphism equations, and coinductive types correspond to their greatest, or final, solutions. Intuitively, the elements of an inductive type are those that may be obtained by a finite composition of its introductory forms. Consequently, if we specify the behavior of a function on each of the introductory forms of an inductive type, then its behavior is determined for all values of that type. Such a function is called a recursor, or catamorphism. Dually, the elements of a coinductive type are those that behave properly in response to a finite composition of its elimination forms. Consequently, if we specify the behavior of an element on each elimination form, then we have fully specified that element as a value of that type. Such an element is called an generator, or anamorphism.

Motivating Examples

The most important example of an inductive type is the type of natural numbers as formalized in Chapter 9. The type nat is defined to be the least type containing z and closed under s(−). The minimality condition is witnessed by the existence of the recursor, iter e {z ⇒ e0 ∣ s(x) ⇒ e1}, which transforms a natural number into a value of type τ, given its value for zero, and a transformation from its value on a number to its value on the successor of that number.

The dynamics of a language is a description of how programs are to be executed. The most important way to define the dynamics of a language is by the method of structural dynamics, which defines a transition system that inductively specifies the step-by-step process of executing a program. Another method for presenting dynamics, called contextual dynamics, is a variation of structural dynamics in which the transition rules are specified in a slightly different manner. An equational dynamics presents the dynamics of a language equationally by a collection of rules for deducing when one program is definitionally equal to another.

Transition Systems

A transition system is specified by the following four forms of judgment:

1. s state, asserting that s is a state of the transition system,

2. s final, where s state, asserting that s is a final state,

3. s initial, where s state, asserting that s is an initial state,

4. s ↦ s′, where s state and s′ state, asserting that state s may transition to state s′.

In practice we always arrange things so that no transition is possible from a final state: If s final, then there is no s′ state such that s ↦ s′. A state from which no transition is possible is sometimes said to be stuck. Whereas all final states are, by convention, stuck, there may be stuck states in a transition system that are not final.

Many programs can be seen as instances of a general pattern applied to a particular situation. Very often the pattern is determined by the types of the data involved. For example, in Chapter 9 the pattern of computing by recursion over a natural number is isolated as the defining characteristic of the type of natural numbers. This concept will itself emerge as an instance of the concept of type-generic, or just generic, programming.

Suppose that we have a function f of type ρ → ρ′ that transforms values of type ρ into values of type ρ′. For example, f might be the doubling function on natural numbers. We wish to extend f to a transformation from type [ρ/t]τ to type [ρ′/t]τ by applying f to various spots in the input where a value of type τ occurs to obtain a value of type ρ′, leaving the rest of the data structure alone. For example, τ might be bool × ρ, in which case f could be extended to a function of type bool × ρ → bool × ρ′ that sends the pairs ⟨a, b⟩ to the pair ⟨a, f(b)⟩.

This example glosses over a significant problem of ambiguity of the extension. Given a function f of type ρ → ρ′, it is not obvious in general how to extend it to a function mapping [ρ/t]τ to [ρ′/t]τ.