Steve Vickers: Research
PhDs under my supervision
If my research topics outlined here are ones that would interest you for PhD study, you are advised to contact me informally before you apply officially through the Admissions Office.
- Qualifications: Normal qualifications expected for admission to a PhD in the School of Computer Science are 2.1 or 1st class honours first degree (or equivalents). However, for the mathematical topics that I would supervise, you would really need a degree at Masters level in maths or a related subject. I shall need to see information about the courses you have taken.
- Special areas: There are two mathematical areas, namely logic and category theory, that are likely to be important in any PhD with me, but at the same time are often absent from maths programmes. At Birmingham you would learn these partly through the week-long Midlands Graduate School in the Foundations of Computer Science, which we mount each year in collaboration with three other universities. Meanwhile, I shall want to know if you have any particuar experience in them.
- For your PhD application you will need to submit a summary of proposed research - the basic area, together with possible ideas. I can discuss the ideas with you so that we know we have a plausible fit.
- Timescale: PhD study can in principle start at any time of the year, but university funding for places begins to be allocated around January and is mostly gone by July. Hence if you must rely on funding from Birmingham then it is better to apply around December - January for admission in October.
With the above in mind, I would ask you to send me -
- A summary of your taught courses taken, with marks where available.
- Samples of your recent dissertation or thesis work so far, or outline proposals for it, something to help me see the level you are currently working at.
- Any particular ideas you have been looking at that might develop to a PhD.
At some stage there will need to be an interview between you, me, and one other member of staff. If you are not able to come to Birmigham, a Skype call is often the most convenient.
You can also find further details on the School's research degree programmes including some information on studentships.
Research
Contents
- Geometric logic
- Toposes
- Sheaves and bundles
- Some of my introductory writings - including Ljubljana tutorial
- More technical issues
- My EPSRC project Applications of geometric logic to topos approaches to quantum theory.
Geometric Logic
"Geometric logic", so-called from its origins in algebraic geometry in the mid 20th century, is an ingenious way to combine two apparently very different mathematical subjects: topology (which studies continuous change) and logic (which studies discrete deduction steps).
Its trick is to take the set-theoretic operations of intersection and (possibly infinite) union, which are used to combine the important open sets of topology, and reinterpret them as logic. Intersection becomes "and", and union becomes "or". Because it has a restricted range of logical connectives it is weaker than the standard "classical" logic of mathematics, though the ability to form "infinite ors" gives it some interesting features.
Under this translation, topological spaces, their points, and continuous maps between the spaces become logical theories, models and interpretations of one theory in another.
The trick of geometric logic arose in fields of pure mathematics, notably algebraic geometry, and led to some interesting "point-free" styles of topology, in which the open sets on a space are defined without knowing in advance what points they are meant to be sets of. The idea has also been used in computer science, where the idea of continuity turns out to be unexpectedly close to that of computability. Then the point-free approach describes spaces of computational objects by logical theories of "how those objects appear to the user" (i.e. what you can know of them by watching them run, as opposed to examining their programs).
Toposes
In essence the trick of geometric logic is a simple one, but it has deep consequences. These arise because the weaker, geometric, logic goes along with a weaker, geometric, mathematics, one that is more compatible with what can be computed. Its constructions have an intrinsic continuity - its weakness is that it cannot do discontinuous things. The study of what can be done in this geometric mathematics leads to the notion of topos.
Topos theory is an astonishingly rich subject dating back to Grothendieck's work on algebraic geometry half a century ago. It has had a profound effect on other fields too, including logic. Partly because of this richness it is notoriously difficult to give a comprehensive conceptual account of what a topos is, but I shall try to explain the way I think of those aspects that enter into my own work.
A topos is analogous to a topological space, but its topological structure cannot be described just using open sets of points. Instead, they must be described by specifying what are the sheaves, or continuous maps from the points to sets. The sheaves are equivalent to the ways of constructing sets from points in the geometric mathematics. This creates a powerful connection between geometric logic and toposes.
A topos is generally said to classify its points, so for example there is a topos that classifies sets, and another that classifies groups.
Toposes can also be understood independently of geometric logic, via another "intuitionistic" logic that is stronger than geometric, but still weaker than classical logic. However, restricting to geometric logic makes it much easier to understand toposes as spaces of points. Much of my work has studied the question of how much practical mathematics can be done within the constraints of geometric logic.
Sheaves and bundles
I said above that a sheaf over a space X can be understood as a continuous map from points of X to sets. The result of this map applied to a point x is called the stalk of the sheaf at x; it is a set. By putting together all the elements of all the stalks one gets another space Y, called the display space, with a map p: Y -> X that shows, for each element of Y, which stalk it comes from.
A map p got in this way is of a special kind, called a local homeomorphism. Thus in a local homeomorphism p: Y -> X, the stalk at any point x of X can be found by looking at the inverse image of x, the set of points y such that p(y) = x. This is also known as the fibre over x.
Now the idea of fibre works for any map p - it does not have to be a local homeomorphism. But in general the fibre has a topology of its own, so we should think of it as a topological space rather than a set. Thus p gets viewed as a variable space (the fibre), varying as the point x varies. From this point of view I shall call p a bundle. (Note for the knowledgeable: I'm not making any other assumptions, such as whether the fibres are non-empty.) Then a sheaf is a bundle in which all the fibres are sets - they have the discrete topology. A sheaf is a "bundle of sets".
Remarkably, the bundle idea still works in point-free topology, and in some ways it actually works even better. The "internal mathematics of toposes" mentioned above, when done for sheaves over X, amounts to a set theory "parametrized by points of X". (This works best when you restrict yourself to the geometric mathematics.) An old and important result of topos theory shows that when you simulate point-free topology in this internal mathematics, you end up with a mathematics of point-free bundles.
In other words, you can discuss bundles in the same way as you discuss spaces, so long as you work (i) point-free, and (ii) in geometric logic. Since geometric logic is weaker than classical logic, this makes it quite interesting to ask how much of ordinary mathematics can be done geometrically. Much of my work has been looking at particular instances of this question.
Some of my introductory writings
The general flavour of using geometric logic is best conveyed in my three-part tutorial on "Formal Topology and Geomeric Logic" (4th Workshop on Formal Topology, Ljubljana, June 2012):
- "Space = geometric theory"
- "Map = geometric transformation of points to points"
- "Bundle = geometric transformation of points to spaces"
Here are some more writings.
- Topology via Logic - my 1988 book introducing (albeit in classical logic) point-free topology, including some computer science applications. Although it doesn't mention geometric logic explicitly, its frame presentations by generators and relations are essentially the same thing as propositional geometric theories.
- Toposes pour les nuls and Toposes pour les vraiments nuls (both actually in English) and Topology via constructive logic are brief summaries of these ideas of using geometric logic to reason about point-free spaces as though they had points.
- Locales and toposes as spaces - a reader's guide to two of the standard topos introductions, from the point of view of geometric logic and points. In fact this big chapter is my first stab at writing a constructive version of "Topology via Logic".
- Fuzzy sets and geometric logic - includes an introduction to sheaves, and the idea that they are "continuous set-valued maps".
- Issues of logic, algebra and topology in ontology describes in detail the "observational" ideas underlying geometric logic.
- "Aspects of Topology" - slides from a talk introducing topology and some of its application in theoretical computer science in the "point-free" form, and then leading on to toposes and a novel use (Imperial, Nijmegen) in the formulation of quantum mechanics.
- "Locales via bundles" - slides from a talk describing the bundle view.
- "Aspects of Geometric Logic" - slides from a talk outlining the role of geometricity, written up as Continuity is Geometricity.
- "Toposes, elephants and gorillas".
More technical issues
As I mentioned, much of my work investigates how ordinary mathematics can be done in geometric logic. The underlying problem is that a point-free space may really not have enough points. In logical terms (point = model of a theory), this is because geometric theories may be incomplete. But that shortage of points is only if the models are sought in ordinary sets. There will always be enough points if you are prepared to seek models in non-standard sets (i.e. in the internal mathematics of toposes). The advantage of geometric logic is that it applies equally well in all those non-standard universes, and transports cleanly between them (technically: it is preserved by inverse image functors of geometric morphisms). Hence by reasoning geometrically you cover also these non-standard points, and of them there are enough.
Many of the ideas are set out in Topical categories of domains, which investigates results known from domain theory and the semantics of computer programming languages (in particular, the results of Samson Abramsky's logical approach). It uses geometric logic to exploit in a deep way the idea of classifying toposes as spaces of points.
An important tool is the theory of powerlocales, or "point-free hyperspaces". (A hyperspace is a space whose points are subspaces of some other space. As powerdomains they have proved an effective tool for discussing non-determinism in computation, since the result of a function then may be a subspace of points rather than a single point.) These give a powerful way to discuss issues such as compactness and I have used them throughout my work. Their good interaction with geometric logic is described in detail in The double powerlocale and exponentiation, which investigates Martin Hyland's famous result from point-free topology on the ability to construct spaces of maps (and, technically, on local compactness).
One important consequence of the infinitary disjunctions in geometric logic is that there is a "geometric type theory" to go with it. An interesting question, discussed in Locales and toposes as spaces, concerns what happens if one combines some of the type theory with the finitary geometric logic, i.e. coherent logic. This is an "arithmetic" logic, and corresponds to using arithmetic universes instead of Grothendieck toposes. Some first results are in An induction principle for consequence in arithmetic universes.