Topology Via LogicNow in paperback, Topology via Logic is an advanced textbook on topology for computer scientists. Based on a course given by the author to postgraduate students of computer science at Imperial College, it has three unusual features. First, the introduction is from the locale viewpoint, motivated by the logic of finite observations: this provides a more direct approach than the traditional one based on abstracting properties of open sets in the real line. Second, the methods of locale theory are freely exploited. Third, there is substantial discussion of some computer science applications. Although books on topology aimed at mathematics exist, no book has been written specifically for computer scientists. As computer scientists become more aware of the mathematical foundations of their discipline, it is appropriate that such topics are presented in a form of direct relevance and applicability. This book goes some way towards bridging the gap. |
Contents
Introduction A Historical Overview | 8 |
Affirmative and refutative assertions In which we see a Logic of Finite Observations and take this as the notion we want to study | 8 |
Frames In which we set up an algebraic theory for the Logic of Finite Observations its algebras are frames | 12 |
32 Posets | 13 |
33 Meets and joins | 14 |
34 Lattices | 18 |
35 Frames | 21 |
36 Topological spaces | 22 |
72 Directed disjunctions of points | 92 |
73 The Scott topology | 95 |
Compactness In which we define conjunctions of points and discover the notion of compactness | 98 |
82 The HofmannMislove Theorem | 100 |
83 Compactness and the reals | 104 |
84 Examples with bit streams | 105 |
85 Compactness and products | 106 |
86 Local compactness and function spaces | 110 |
37 Some examples from computer science | 23 |
Different physical assumptions | 27 |
Flat domains | 28 |
Function spaces | 29 |
38 Bases and subbases | 31 |
39 The real line | 32 |
310 Complete Heyting algebras | 34 |
Frames as algebras In which we see methods that exploit our algebraicizing of logic | 38 |
42 Generators and relations | 39 |
43 The universal characterization of presentations | 42 |
44 Generators and relations for frames | 46 |
Topology the definitions In which we introduce Topological Systems subsuming topological spaces and locales | 52 |
52 Continuous maps | 54 |
53 Topological spaces | 57 |
Spatialization | 59 |
54 Locales | 60 |
Localification | 62 |
55 Spatial locales or sober spaces | 65 |
56 Summary | 68 |
New topologies for old In which we see some ways of constructing topological systems and some ways of specifying what they construct | 70 |
62 Sublocales | 71 |
63 Topological sums | 76 |
64 Topological products | 80 |
Point logic In which we seek a logic of points and find an ordering and a weak disjunction | 89 |
Spectral algebraic locales In which we see a category of locales within which we can do the topology of domain theory | 116 |
92 Spectral locales | 119 |
93 Spectral algebraic locales | 121 |
94 Finiteness second countability and coalgebraicity | 125 |
95 Stone spaces | 128 |
Domain Theory In which we see how certain parts of domain theory can be done topologically | 134 |
102 Bottoms and lifting | 136 |
103 Products | 138 |
104 Sums | 139 |
105 Function spaces and Scott domains | 142 |
106 Strongly algebraic locales SFP | 147 |
107 Domain equations | 152 |
Power domains In which we investigate domains of subsets of a given domain | 165 |
112 The Smyth power domain | 166 |
113 Closed sets and the Hoare power domain | 169 |
114 The Plotkin power domain | 171 |
115 Sets implemented as lists | 176 |
Spectra of rings In which we see some old examples of spectral locales | 181 |
122 Quantales and the Zariski spectrum | 182 |
123 Cohns field spectrum | 185 |
Bibliography | 191 |
196 | |
Common terms and phrases
Abramsky Alexandrov topology axioms bilimit Boolean algebra bottom C-ideal closed sets compact elements compact open compact points compact sets Computer Science congruence construct continuous map coprime coprime decomposition corresponding countable dcpo deduce defined Definition directed joins disjunction distributive lattice domain equation domain theory equivalent Exercise false finite observations finite set finite subset fixpoints frame homomorphism function spaces functor Hausdorff hence Idl(P infinite isomorphic Lemma logic matrix ideals meets and joins Nf(b open sets Plotkin poset power domain preorder presented preserves finite meets Proof Let Proposition pt f(x quantale quasicoprimes reflective embedding refutative satisfies Scott domain Scott open filters Scott topology semilattice sequence set of compact set of points Smyth sober spaces spectral algebraic locale spectral locale starts subbasic sublocale Suppose Theorem topological space topological system true unique universal property w-chain