Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Steve Vickers's WWW Home Page
Teaching
I am Research Students Tutor. (Here is a link to
information for current research students.)
I do not deal with admissions to research degree programmes
(PhD or MPhil in Computer Science or Cognitive Science) -
our admissions page is
here.
I teach -
I also have lecture notes for research seminars I have given (primarily
for PhD students) on Category Theory and
"Topology via Logic".
Check my personal timetable if you want
to
check when I am likely to be free.
Research
I am a member of the Mathematical
Foundations of Computer Science research group.
My particular research interests are in geometric logic, topology and
topos theory.
Before I joined Birmingham I was at the Department of Pure Maths
at
the Open University, and before
that I was at the Department of
Computing at Imperial College,
where I worked in the Theory and
Formal Methods group.
You can download many of my papers
and talks, and also
theses of some of my former PhD students.
Geometric Logic
Most of my work is in investigating "geometric logic" (so-called from
its origins in algebraic geometry). This has some unusual properties.
First, it makes a hard distinction between formulae and axioms: a
logical formula is restricted in the connectives it can use, to
conjunction, disjunction, equality and existential quantification, and
an axiom (for a geometric theory) expresses relationships between
formulae in the form "for all x, y, z, ... (formula1 - formula2)".
Hence
the missing connectives can be introduced in just one layer - no
nesting
- in axioms. Second, it allows infinite disjunctions in formulae.
Though these features may look weird, they have some conceptual
justification in the idea of observation: formulae correspond to
observable facts (and infinite disjunction is not a problem
observationally) while the axioms correspond to background assumptions
or scientific hypotheses.
A particularly pleasing property of the logic is its close
relationship with topology: the class of models for a propositional
geometric theory is automatically a topological space, and by working
within a "geometrically" constrained constructivist mathematics, one
finds that constructions of functions from one such space to another
are
automatically continuous - indeed, with a bit of oversimplification, I
have argued ("Toposes pour les vraiment nuls")
that
since "geometric mathematics" is intrinsically continuous, it is only
to
compensate for the over-optimism of classical reasoning that one needs
explicit topologies and continuity proofs. This "topology-free space"
approach leads naturally, by generalizing to the predicate logic, to
Grothendieck's toposes as generalized topological spaces.
To work with "topology-free spaces" is to accept certain
constructivist constraints on one's mathematics, and a number of my
more
theoretical papers (in particular "Topical
Categories
of Domains" and "Localic Completion of Quasimetric Spaces") serve as
case studies to investigate whether the constraints still permit
sensible mathematics.
A number of features suggest that the ideas may be applicable to
specification of computer systems:
- the propositional geometric logic has already found computer
science application in denotational semantics;
- the constructivism suggests a good fit with computation;
- the observational intuitions fit the idea that a specification
must also describe those aspects of the real world that are relevant to
the computer system in use;
- the good fit with topology promises better ways to integrate
specification with continuous and real number issues, and with
semantics
(which are so often topological);
and some preliminary work has been done on how geometric logic might be
used as a specification language.
A key part of this application would be to remove the infinities
from the logic, so that support tools can be based on a finitary
formalism. To some extent this can be done by introducing inductive
sort
constructors in the many-sorted predicate logic: then propositional
theories with infinite disjunctions can often be replaced by equivalent
finite predicate theories in which the sorts are specified as being
constructed in a given way. A promising mathematical approach to this
is
by the category of Joyal's "Arithmetic Universes".
Related to this field is my lecture Non-classical
Reasoning, which was given as a first year undergraduate "Topics"
lecture in the Department of Computing at Imperial College.
Lectures on Category Theory and Topology
via Logic
In 2003-4 I gave two series of talks aimed primarily at research
students. Copies of my slides are available from me.
The first series was on Category Theory, and comprised lectures I gave
at Imperial introducing categories as part of an MSc module on
Mathematical Structures for Computer Science.
The second series developed the ideas of my book Topology via Logic (Cambridge
University Press 1989, ISBN 0 521 36062 5 and 0 521 57651 2), which was
an introduction to topology and its use in computer science.
In many ways the lectures followed the book, but they went beyond it in
bringing out the deep relationship with constructive logic. Part of
their aim was to put together the shape of a constructive 2nd edition
of Topology via Logic.
Outline
"via Logic"
In my book, "via Logic" referred to the way it presents topologies as
Lindenbaum algebras for theories in a particular non-classical logic,
the so called geometric logic.
This lies behind an alternative approach to topology known as locale
theory, which has been used in the semantics of programming languages -
notably in Abramsky's thesis.
Observability
In my book I motivate the use of geometric logic by an informal
discussion of how certain logical connective have observational content
(this is also present in the work of Smyth and Abramsky). Then the
basic
deal in semantics is that a domain, with its Scott topology, embodies a
logical theory of how one can observe some type of program by watching
it run (without access to the source code).
Going constructive
The book is entirely classical in its mathematics. However, since it
was written I have come to understand much better the key role of
constructive mathematics in topology and have exploited it in my papers
such as "Topical categories of domains". This is what I want to explain
in the lectures.
Better constructive topology
One aspect of this is that if you are already committed to
constructivism (maybe in order to take better account of computational
issues), then the localic approach is known to give better results in
constructive topology than topology itself.
Continuity for free
But there are deeper reasons topological reasons for being
constructive. Associated with the geometric logic, there is a
"geometric
mathematics". It is constructive, and also has an intrinsic continuity.
If you adhere to the constructive constraints of geometric reasoning
then you do not have to give explicit continuity proofs - continuity is
automatic. In effect, the usual continuity proofs in classical
reasoning
are bureaucratic certifications that you haven't transgressed the
geometric constraints. So there are quite practical reasons for
accepting those constraints.
Toposes
A major spinoff is that the same approach adapts quite naturally to a
generalization of topological space, namely toposes. This aspect of
toposes is normally concealed, but it is fundamental to their
importance. Roughly speaking, from this point of view a (Grothendieck)
topos is a topological space for which there are "not enough opens" and
instead the topological structure has to be defined through what are
known as its sheaves.
Downloadable papers
Below are preprint versions of some of my papers, the most recent
first. A more complete list (with
abstracts and
citation details) is also available.
(with Achim Jung and Drew Moshier) "Presenting dcpos and dcpo algebras"
describes the presentations of dcpo algebras by generators and relations.
"Issues of logic, algebra and topology in ontology"
uses geometric logic as a case study for how a logic might be affected by the
ontological commitment one is prepared to make.
"Fuzzy sets and geometric logic"
describes how geometric logic can provide a conceptual simplification of Hoehle's
sheaf approach to fuzzy sets.
You can also download
slides of my
Linz talk on this topic.
"Cosheaves and connectedness in formal topology"
gives a predicative introduction to some topos ideas in Bunge and Funk's
book "Singular Coverings of Toposes".
"A localic
theory of lower and upper integrals" is just what it says.
"The connected Vietoris powerlocale" describes
a powerlocale construction whose points are connected,
and uses it to give a choice-free constructive account of the Intermediate
Value Theorem and Rolle's Theorem.
"Locales and toposes as spaces" is a
first step towards a constructive version of "Topology via Logic". It
explains how theories in geometric logic can be viewed as topological
spaces (for the propositional fragment) or generalized topological
spaces (toposes) for the full
predicate logic.
(with Erik Palmgren) "Partial Horn logic
and cartesian categories" gives a simple presentation of cartesian
theories using a logic in which function symbols may be partial. It
leads to an easy proof of the free model theorem, and a simple
construction of classifying categories.
"Sublocales in formal topology" shows how
various results about
sublocales in topos-valid locale theory transfer to predicative
formal topology.
"Some constructive roads to Tychonoff"
uses Tychonoff's theorem as a case study for approaches to topology in
constructive mathematics. The final version is published in this book.
(with Gillian Hill) "A language for configuring
multi-level specifications" develops "Presheaves
as configured specifications" to cope with specifications in which
components of systems may themselves be configured systems.
"Localic
completion of generalized metric
spaces I" shows how generalized metric spaces may be completed to
give locales. "Generalized" means esentially that only the zero
self-distance and the triangle inequality are expected. "Localic completion of generalized metric spaces II:
Powerlocales" investigates their powerlocales, gives a simple
description of them as "generalized metric powerspaces", and describes
some application.
"Entailment systems for stably locally
compact locales" describes a way of presenting stably locally
compact locales using a kind of non-reflexive sequent calculus. It is
similar to the Multilingual Sequent Calculus of Jung, Kegelmann and
Moshier, but without the explicit presence of conjunction and
disjunction in the sequents.
(with Christopher Townsend) "A universal
characterization of the double powerlocale" shows that the double
powerlocale PP(X) can be
considered a double exponential $^($^X)
even when X is not locally
compact (so $X
doesn't exist). It does this using the Yoneda embedding of the category
of locales.
"Compactness in locales and in formal topology"
describes a general criterion for compactness of a formal topology
(with preordered base) and proves it in both topos-valid mathematics
and
predicative mathematics.
"The
double powerlocale and exponentiation: a case study in geometric logic"
examines the "double powerlocale", the composite of the upper and lower
powerlocales, and relates it to exponentiation. It uses geometric
reasoning (stable under pullback along geometric morphisms) to make
locales appear like spaces.
(with Pedro Resende) "Localic
sup-lattices and tropological systems" resets the quantale methods in a constructive localic
framework.
(with Gillian Hill) "Presheaves
as Configured Specifications" outlines a specification language for
describing how components are put together with sharing. It uses
presheaves to give a mathematical treatment that is both simple and
specificationally natural.
"Strongly Algebraic = SFP (Topically)" develops
the work of "Topical Categories of Domains" to cover
the equivalence between two of Plotkin's characterizations of SFP
domains. It also serves as an introduction to how presheaf toposes are
interpreted as generalized spaces.
"Localic Completion of Quasimetric Spaces"
presents a localic account of completion of quasimetric spaces, using
Lawvere's approach by enriched categories.
"Topical Categories of
Domains" sets domain theory, and in particular Abramsky's account
in "Domain Theory in Logical Form", in a framework of geometric logic.
Ordinary categories of domains are replaced by "topical" categories,
internal in the category of toposes and geometric morphisms: the
classes
of objects and morphisms are replaced by toposes classifying them.
"Topology via Constructive Logic" presents the
idea that constructive mathematics has practical usefulness in studying
topology.
"Constructive points of powerlocales"
gives a constructively sound account of the points of the lower, upper
and Vietoris powerlocales, and shows how in certain cases a powerlocale
of D is homeomorphic to $^D.
"Toposes pour les vraiment
nuls" is a further introduction to Grothendieck's idea of toposes
as generalized topological spaces, using geometric logic to hide
topology.
"Toposes pour les nuls" is a brief
introduction to Grothendieck's idea of toposes as generalized
topological spaces, written from a topological viewpoint.
"Locales are not pointless" presents some
preliminary results for reasoning about arbitrary locales through their
points, with particular applications to powerlocales.
(With Mark Dawson) "Towards a GeoZ toolkit"
discusses how a mathematical toolkit for GeoZ must differ from that for
Z, and illustrates the use of schema entailment in presenting it.
"Geometric logic as a specification language"
is a short introduction to GeoZ, a Z-like specification language based
on geometric logic. Includes a description of "schema entailment" and
its use as a definitional mechanism.
"Geometric Logic in Computer Science" is
an introduction to geometric logic, paying particular attention to the
deep mathematical properties that make it differ from other logics.
(With Samson Abramsky) "Quantales, Observational Logic and Process
Semantics" studies quantales (complete lattices equipped with
monoid structure, the binary operation distributing over all joins)
with
applications to process semantics.
"Information Systems for Continuous Posets"
defines an "infosys" as an idempotent relation, and shows how they may
be used to present continuous dcpos. Includes a proof that the Vietoris
powerlocale of a continuous dcpo is again a continuous dcpo.
"Geometric Theories and Databases"
describes a topos-theoretic construction of categorical powerdomains
(bagtoposes) with tentative application to database theory.
(With Peter Johnstone) "Preframe
Presentations Present" investigates preframes (directed complete
posets with finite meets that distribute over the directed joins) with
applications to locale theory, including an easy proof of the localic
Tychonoff theorem.
Talks
"Aspects of Topology" (Departmental Seminar, School of Computer Science, University of Brimingham) - Introduces topology and some of its application in theoretical computer science in the "point-free" form, and then leads on to toposes and a novel use (Imperial, Nijmegen) in the formulation of quantum mechanics.
"On the Trail of the Formal Topos" -
Advances in Constructive Topology and Logical Foundations,
Padua 8-11 October 2008.
Discusses routes for extracting predicative content from topos theory.
"Locales via Bundles" -
Sheaves in Geometry and
Quantum Theory, Nijmegen 3-5 Spetember 2008;
slightly briefer version given at
Categories, Logic
and Physics, Oxford, 23-24 August 2008. Introduces locales through the idea of bundles, with reference to the topos approaches to quantum theory.
"Fuzzy Sets and Geometric Logic" -
29th
Linz Seminar on Fuzzy Set Theory: Foundations of Lattice-Valued Mathematics
with Applications to Algebra and Topology, Linz 12-16 February 2008.
Explains sheaf accounts of fuzzy sets in terms of geometric logic.
"Schemas as
Toposes" - Open University on 2nd July 2002.
Past PhD students
(New PhD students welcome!)