# Steve Vickers: Bibliography

# Steven Vickers: Bibliography

This is a complete list of my academic papers, with abstracts and dowloadable preprint versions where available.

Elsewhere, you can also find -

- a briefer summary of the papers
- slides from selected talks
- a list of my papers in bibtex format
- links to papers of my PhD students

#### Note on .ps papers

Some of the older .ps papers (PreFrPrePre, GeoTh+DBs, Infosys and QuProc) have been prepared from original Microsoft Word documents. They will differ from the published versions, certainly in format and perhaps also in details of content. Also, some of those .ps files have not been tested on a printer, so please report any problems with them by emailing me (s.j.vickers) at cs.bham.ac.uk.

## Contents (most recent first)

- The localic compact interval is an Escardó-Simpson interval object
- A coherent account of geometricity
- Geometric constructions preserving fibrations
- Positivity relations on a locale
- Gelfand spectra in Grothendieck toposes using geometric mathematics
- The Born rule and structure of spectral bundles
- A monad of valuation locales
- Continuity and geometric logic
- Generalized powerlocales via relation lifting
- An induction principle for consequence in arithmetic universes
- Presenting dcpos and dcpo algebras
- Issues of logic, algebra and topology in ontology
- Fuzzy sets and geometric logic
- Cosheaves and connectedness in formal topology
- A localic theory of lower and upper integrals
- The connected Vietoris powerlocale
- Locales and toposes as spaces
- Partial Horn logic and cartesian categories
- Sublocales in formal topology
- Some constructive roads to Tychonoff
- A language for configuring multi-level specifications
- Localic completion of generalized metric spaces II: Powerlocales
- Localic completion of generalized metric spaces I
- Entailment systems for stably locally compact locales
- A universal characterization of the double powerlocale
- Compactness in locales and in formal topology
- The double powerlocale and exponentiation: a case study in geometric logic
- Localic sup-lattices and tropological systems
- Presheaves as Configured Specifications
- Strongly Algebraic = SFP (Topically)
- Localic Completion of Quasimetric Spaces
- Topical Categories of Domains
- Topology via Constructive Logic
- Toposes pour les vraiment nuls
- Constructive points of powerlocales
- Toposes pour les nuls
- Reasoned Programming
- Locales are not pointless
- Geometric logic as a specification language
- Towards a GeoZ toolkit
- Geometric Logic in Computer Science
- Quantales, Observational Logic and Process Semantics
- Information Systems for Continuous Posets
- Geometric Theories and Databases
- Preframe Presentations Present
- Formal Implementation
- Topology Via Logic
- A fixpoint construction of the
*p*-adic domain - An algorithmic approach to the
*p*-adic integers - Theories as categories

### ABSTRACTS

#### "The localic compact interval is an Escardó-Simpson interval object"

Unpublished.

Preprint version June 2015: pdf.

The locale corresponding to the real interval $[-1,1]$ is an interval object, in the sense of Escard\'{o} and Simpson, in the category of locales. The map $c\colon 2^\omega \to [-1,1]$, mapping a stream $s$ of signs $\pm 1$ to $\Sigma_{i=1}^\infty s_i 2^{-i}$, is a proper localic surjection; it is also expressed as a coequalizer.

#### "A coherent account of geometricity"

(Steven Vickers and Christopher Townsend)

Unpublished.

Preprint version April 2014: pdf.

A "bundle endofunctor preserving proneness" for a cartesian category $\mathcal{C}$
is an endofunctor $\mathfrak{T}_\bullet$ of the arrow category $\mathcal{C}^{\downarrow}$,
the identity on codomains, that preserves the property of morphisms of being pullback squares.
Such a $\mathfrak{T}_\bullet$ is "slicewise strong",
restricting to a strong endofunctor $\mathfrak{T}_\bullet$ on every slice $\mathcal{C}/B$,
and with that structure preserved by pullback between slices.

In the other direction, a strong endofunctor $T$ on $\mathcal{C}$ extends to a bundle endofunctor
$T_\bullet$ on $\mathcal{C}$, which preserves proneness if $T$ preserves coreflexive equalizers.

If a bundle endofunctor $\mathfrak{T}_\bullet$ preserving proneness also preserves coreflexive equalizers,
then it is naturally isomorphic to the $T_\bullet$ arising from $T = \mathfrak{T}_1$.

Combining these, bundle endofunctors for $\mathcal{C}$ preserving proneness and coreflexive equalizers
are equivalent to strong endofunctors on $\mathcal{C}$ preserving coreflexive equalizers;
this latter structure is inherited by all slices and preserved by pullback between them.

The results extend to situations where $\mathfrak{T}_\bullet$ and $T$ are monads.

We propose that the structure of bundle endofunctor preserving proneness is a satisfactory
categorical abstraction of the notion of geometric construction when $\mathcal{C}$ is the
category $\mathbf{Loc}$ of locales.
The powerlocales give rise to bundle monads on $\mathbf{Loc}$ preserving proneness
and coreflexive equalizers;
likewise for the covariant powerobject monad on any topos.

#### "Geometric constructions preserve fibrations"

(Bertfried Fauser and Steven Vickers)

Unpublished.

Archived at arXiv:1411.2457.

Let $\mathcal{C}$ be a representable 2-category, and $\mathfrak{T}_\bullet$ a 2-endofunctor of the arrow 2-category $\mathcal{C}^\downarrow$ such that (i) $\mathsf{cod} \mathfrak{T}_\bullet = \mathsf{cod} \colon \mathcal{C}^\downarrow \rightarrow \mathcal{C}$ and (ii) $\mathfrak{T}_\bullet$ preserves proneness (cartesianness) of morphisms in $\mathcal{C}^\downarrow$. Then $\mathfrak{T}_\bullet$ preserves fibrations and opfibrations in $\mathcal{C}$. The proof takes Street's characterization of (e.g.) opfibrations as pseudoalgebras for 2-monads $\mathfrak{L}_B$ on slice categories $\mathcal{C}/B$ and develops it by defining a 2-monad $\mathfrak{L}_\bullet$ on $\mathcal{C}^\downarrow$ that takes change of base into account, and uses known results on the lifting of 2-functors to pseudoalgebras.

#### "Positivity relations on a locale"

(Francesco Ciraulo and Steven Vickers)

Annals of Pure and Applied Logic,
special issue for articles on the topics of the
4th Workshop on Formal Topology (4WFTop), Ljubljana 2012.

Published on-line 20-Apr-2016

ISSN 0168-0072,

doi:10.1016/j.apal.2016.04.009

Final submitted version January 2015: pdf.

This paper analyses the notion of a *positivity relation*
of Formal Topology from the point of view of the theory of Locales. It is shown that a positivity relation on a locale corresponds
to a suitable class of points of its lower powerlocale.
In particular, closed subtopologies associated to the
positivity relation correspond to overt
(that is, with open domain) weakly closed sublocales.
Finally, some connection is revealed between positivity
relations and localic suplattices
(these are algebras for the powerlocale monad).

#### "Domain theory in topical form"

In Coecke, Ong, Panangaden (ed.)
"Computation, Logic, Games, and Quantum Foundations.
The Many Facets of Samson Abramsky"

Springer LNCS **7860** (2013), pages 348--349

ISSN 0302-9743, ISBN 978-3-642-38163-8,

doi:10.1007/978-3-642-38164-5_24

Preprint version: pdf.

Describes how "Topical categories of domains" developed out of Abramsky's "Domain theory in logical form".

#### "Gelfand spectra in Grothendieck toposes using geometric mathematics"

(Bas Spitters, Steven Vickers and Sander Wolters)

In *Proceedings of the 9th International Workshop on Quantum Physics and Logic (QPL 2012)*, Brussels 2012
(ed. Duncan, Panangaden).

Electronic Proceedings in Theoretical Computer Science
**158** (2014), pp. 77 - 107.

ISSN 2075-2180,
doi:10.4204/EPTCS.158.7

Preprint version: pdf, or arXiv 1310.0705.

In the topos approach to quantum theory by Heunen, Landsman and Spitters, one associates to any
unital C*-algebra *A*, a topos *T(A)*
of sheaves on a locale and a commutative C*-algebra A within
that topos.
The Gelfand spectrum of A is a locale Σ
in this topos, which is equivalent to a bundle
over the base locale. We further develop this external presentation of the locale Σ, by noting that the
construction of the Gelfand spectrum in a general topos can be described using geometric logic.
As a consequence, the spectrum, seen as a bundle, is computed fibrewise.

As a by-product of the geometricity of Gelfand spectra,
we find an explicit external description
of the spectrum whenever the topos is a functor category.
As an intermediate result we show that
locally perfect maps compose, so that the externalization of a locally compact locale in a topos of
sheaves over a locally compact locale is locally compact, too.

#### "The Born rule as structure of spectral bundles"

(Extended abstract)

(Bertfried Fauser, Guillaume Raynaud and Steven Vickers)

In *Proceedings of the 8th International Workshop on Quantum Physics and Logic (QPL 2011)*, Nijmegen 2011
(ed. Jacobs, Selinger, Spitters).

Electronic Proceedings in Theoretical Computer Science
**95** (2012), pp. 81 - 90.

ISSN 2075-2180,
doi:10.4204/EPTCS.95.8

Preprint version: pdf

Topos approaches to quantum foundations are described in a unified way by means of spectral bundles, where the base space is a space of contexts and each fibre is its spectrum. Differences in variance are due to the the bundle being a fibration or opfibration. Relative to this structure, the probabilistic predictions of the Born rule in finite dimensional settings are then described as a section of a bundle of valuations. The construction uses in an essential way the geometric nature of the valuation locale monad.

#### "A monad of valuation locales"

Preprint version: pdf

If *X* is a locale then its valuation locale has for its points the valuations on
*X*. This construction is the functor part of a strong monad on the category of
locales, a localic analogue of the Giry monad. It is commutative, i.e. product valuations
exist and a Fubini Theorem holds. An analogue of the Riesz Representation theorem holds.
Concrete representations are given for the tensor product of lattices and for
the modular monoid. The work conforms with the constructive constraints of
geometric logic.

#### "Continuity and geometric logic"

Journal of Applied Logic **12 (1)** (2014), pages 14-27

ISSN: 1570-8683; doi: 10.1016/j.jal.2013.07.004.

Preprint version: pdf

Reports my Bordeaux talk
"Aspects of geometric logic".

This paper is largely a review of known results about various aspects of geometric logic. Following Grothendieck's view of toposes as generalized spaces, one can take geometric morphisms as generalized continuous maps. The constructivist constraints of geometric logic guarantee the continuity of maps constructed, and can do so from two different points of view: for maps as point transformers and maps as bundles.

#### "Generalized powerlocales via relation lifting"

(Yde Venema, Steven Vickers and Jacob Vosmaer)

Mathematical Structures in Computer Science
**23 (1)** (2013), pages 142-199.

ISSN: 0960-1295; doi: 10.1017/S0960129512000229.

Preprint version: pdf

This paper introduces an endofunctor *V _{T}* on the category of frames, parametrized by
an endofunctor

*T*on the category Set that satisfies certain constraints. This generalizes Johnstone's construction of the Vietoris powerlocale, in the sense that his construction is obtained by taking for

*T*the finite covariant power set funtor. Our construction of the

*T*-powerlocale

*V*out of a frame

_{T}L*L*is based on ideas from coalgebraic logic and makes explicit the connection between the Vietoris construction and Moss's coalgebraic cover modality.

We show how to extend certain natural transformations between set functors to natural transformations between *T*-powerlocale functors.
Finally, we prove that the operation *V _{T}* preserves
some properties of frames, such as regularity, zero-dimensionality, and the combination of zerodimensionality
and compactness.

#### "An induction principle for consequence in arithmetic universes"

(Maria Emilia Maietti and Steven Vickers)

Journal of Pure and Applied Algebra
**216 (8-9)** (2012), pages 2049-2067.

ISSN: 0022-4049; doi: 10.1016/j.jpaa.2012.02.040.

Preprint version: pdf

Presentations: Amsterdam and
Genova.

Suppose in an arithmetic unverse we have two predicates φ and ψ for
natural numbers, satisfying a base case φ(0)→ψ(0) and an
induction step that, for generic *n*, the hypothesis
φ(*n*)→ ψ(*n*)
allows one to deduce
φ(*n*+1)→ ψ(*n*+1).
Then it is
already true in that arithmetic universe that
(∀ *n*)(φ(*n*)→ ψ(*n*)).
This is substantially harder than in a topos, where cartesian
closedness allows one to form an exponential
φ(*n*)→ ψ(*n*).

The principle is applied to the question of locatedness of Dedekind sections.

The development analyses in some detail a notion of "subspace" of an arithmetic universe, including open or closed subspaces and a boolean algebra generated by them. There is a lattice of subspaces generated by the opens and the closeds, and it is isomorphic to the free Boolean algebra over the distributive lattice of subobjects of 1 in the arithmetic universe.

#### "Presenting dcpos and dcpo algebras"

(Achim Jung, M. Andrew Moshier and Steven Vickers)

In *Proceedings of the 24th Conference on the Mathematical
Foundations of Programming Semantics (MFPS XXIV)*
(ed. Bauer, Mislove),
Electronic Notes in Theoretical Computer Science
**218** (2008), pp. 209 - 229.

ISSN 1571-0661;
doi:10.1016/j.entcs.2008.10.013

Preprint version: pdf

Dcpos can be presented by a preorder of generators and inequational relations expressed as covers. Algebraic operations on the generators (possibly with their results being ideals of generators) can be extended to the dcpo presented, provided the covers are "stable" for the operations. The resulting dcpo algebra has a natural universal characterization and satisfies all the inequational laws satisfied by the generating algebra.

Applications include known "coverage theorems" from locale theory.

#### "Issues of logic, algebra and topology in ontology"

Chapter 22 in
"Theory
and Applications of Ontology: Computer Applications"
(ed. Poli, Healy, Kameas),
vol. 2 of "Theory and Applications of Ontology", Springer, 2010.

ISBN 978-90-481-8846-8

Copyright Springer.

Preprint version: pdf

When one uses a particular logical formalism, one makes an *ontological
commitment* to being able to interpret the symbols involved. We discuss this
in a case study of geometric logic, being aided by a presentation of the logic
as a sequent calculus. We also discuss the connections of geometric logic with
topology and algebra.

#### "Fuzzy sets and geometric logic"

Fuzzy Sets and Systems **161** (2010), pp. 1175 - 1204.

ISSN 0165-0114;
doi:
10.1016/j.fss.2009.06.013.

Preprint version: pdf

Hoehle has identified fuzzy sets, valued in a frame (complete Heyting algebra) Ω, with certain sheaves over Ω: the subsheaves of constant sheaves More general sheaves can be got as quotients of the fuzzy sets. His principal approach to sheaves over Ω, and topos-theoretic constructions on them, is via complete Ω-valued sets.

In this paper we show how the *geometric* fragment of those constructions
can be described in a natural "stalkwise" manner, provided one works also
with incomplete Ω-valued sets.

Our exposition examines in detail the interactions between different technical expressions of the notion of sheaf, and highlights a conceptual view of sheaf as "continuous set-valued map".

You can also view my slides for the invited talk I gave on this topic at the 29th Linz Seminar on Fuzzy Set Theory, February 2008.

#### "Cosheaves and connectedness in formal topology"

Annals of Pure and Applied Logic **163** (2012), pp. 157-174.

ISSN 0168-0072;
doi:10.1016/j.apal.2011.06.024

Preprint version: pdf

The localic definitions of cosheaves, connectedness and local connectedness
are transferred from impredicative topos theory to predicative formal
topology. A formal topology is locally connected (has base of connected opens)
iff it has a cosheaf π_{0} together with certain additional structure and
properties that constrain π_{0} to be the connected components cosheaf. In
the inductively generated case, complete spreads (in the sense of Bunge and
Funk) corresponding to cosheaves are defined as formal topologies. Maps
between the complete spreads are equivalent to homomorphisms between the
cosheaves. A cosheaf is the connected components cosheaf for a locally
connected formal topology iff its complete spread is a homeomorphism, and in
this case it is a terminal cosheaf.

A new, geometric proof is given of the topos-theoretic result that a cosheaf
is a connected components cosheaf iff it is a "strongly terminal" point of
the symmetric topos, in the sense that it is terminal amongst all the
*generalized* points of the symmetric topos. It is conjectured that a
study of sites as "formal toposes" would allow such geometric proofs to be
incorporated into predicative mathematics.

*Key words:* Formal topology, predicative, locally connected,
cosheaf, symmetric topos, complete spread

*2008 MSC:* Primary 03F60; Secondary 54D05, 54B20, 18F10

#### "A localic theory of lower and upper integrals"

Mathematical Logic Quarterly **54 (1)** (2008), pp. 109 - 123.

ISSN 0942-5616 (print), 1521-3870 (online);
doi:10.1002/malq.200710028

Preprint version: pdf

An account of lower and upper integration is given. It is constructive in the sense of geometric logic. If the integrand takes its values in the non-negative lower reals, then its lower integral with respect to a valuation is a lower real. If the integrand takes its values in the non-negative upper reals, then its upper integral with respect to a covaluation and with domain of integration bounded by a compact subspace is an upper real. Spaces of valuations and of covaluations are defined.

Riemann and Choquet integrals can be calculated in terms of these lower and upper integrals.

#### "The connected Vietoris powerlocale"

Topology and its Applications **156** (2009), pp. 1886-1910.

ISSN: 0166-8641;
doi:10.1016/j.topol.2009.03.043

Preprint version: pdf

The Vietoris powerlocale *VX*
is a point-free analogue of the Vietoris
hyperspace. In this paper we introduce and study a sublocale
*V ^{c}X* whose
points are those points of

*VX*that (considered as sublocales of

*X*) satisfy a constructively strong connectedness property.

*V*is a strong monad on the category of locales. The strength gives rise to a product map

^{c}Xx:

*V*x

^{c}X*V*->

^{c}Y*V*(

^{c}*X*x

*Y*),

showing that the product of two of these connected sublocales is again connected. If

*X*is locally connected then

*V*is overt. In the case where

^{c}X*X*is the localic completion of a generalized metric space

*Y*, the points of

*V*are characterized as certain Cauchy filters of formal balls for the finite power set F

^{c}X*Y*with respect to a Vietoris metric.

The results are applied to the particular case of the point-free real line, giving a choice-free constructive version of the Intermediate Value Theorem and Rolle's Theorem.

The work is constructive in the sense of topos-validity with natural numbers object. Its geometric aspects (preserved under inverse image functors) are stressed, and exploited to give a pointwise development of the point-free locale theory. The connected Vietoris powerlocale itself is a geometric construction.

#### "Locales and toposes as spaces"

Chapter 8 in "Handbook of Spatial Logics" (ed. Aiello,
Pratt-Hartman, van Bentham), Springer, 2007, pp. 429-496.

ISBN 978-1-4020-5586-7

Copyright Springer Science + Business Media
B.V.

Preprint version: pdf

This chapter was written as an introduction for logicians to the spatial content of geometric logic.

It first outlines the established ideas of Lindenbaum algebras of logical theories, and how they combine with Stone duality (between Boolean algebras and Stone topological spaces) to give a correspondence between theories in classical propositional logic and Stone spaces. This enables one to treat logical theories as topological spaces.

The aim of the chapter is to show how the same insights can be applied to geometric logic, whose connectives mirror the axioms of topology, even though its incompleteness means there is no exact Stone duality.

An important part of this is the role of constructive reasoning. This is paradoxical, since without classical principles (such as choice) it becomes even harder to find the models needed to show completeness. However, constructive reasoning can be applied to models in non-classical mathematics, and in particular the internal mathematics of sheaves. This has the effect of allowing access to a sufficiency of models.

The chapter also describes how the same principles apply to theories in predicate geometric logic. However, the spaces are now generalized in Grothendieck's sense as toposes. The chapter describes how the categorical technicalities of topos theory (e.g. in Mac Lane and Moerdijk) connects to the spatial intuitions.

#### "Partial Horn logic and cartesian categories"

(Erik Palmgren and Steven Vickers)

Annals of Pure and Applied Logic **145 (3)** (2007), pp. 314 - 353.

ISSN: 0168-0072;
doi:10.1016/j.apal.2006.10.001

Preprint version: pdf

A logic is developed in which function symbols are allowed to represent partial functions. It has the usual rules of logic (in the form of a sequent calculus) except that the substitution rule has to be modified. It is developed here in its minimal form, with equality and conjunction, as "partial Horn logic".

Various kinds of logical theory are equivalent:

- partial Horn theories
- "quasi-equational" theories, partial Horn theories without predicate symbols
- cartesian theories
- essentially algebraic theories

The logic is sound and complete with respect to models in $\mathbf{Set}$, and sound with respect to models in any cartesian (finite limit) category.

The simplicity of the quasi-equational form allows an easy predicative constructive proof of the free partial model theorem for cartesian theories: that if a theory morphism is given from one cartesian theory to another, then the forgetful (reduct) functor from one model category to the other has a left adjoint.

Various examples of quasi-equational theory are studied, including those of cartesian categories and of other classes of categories. For each quasi-equational theory $\mathbb{T}$ another, $\mathrm{Cart}\varpi\mathbb{T}$, is constructed, whose models are cartesian categories equipped with models of $\mathbb{T}$. Its initial model, the "classifying category" for $\mathbb{T}$, has properties similar to those of the syntactic category, but more precise with respect to strict cartesian functors.

MSC: Primary 18C10. Secondary 03C05, 03G30, 08A55, 08B05, 08B20, 18C05.

*Keywords:*
Cartesian theory, essentially algebraic, free algebra, classifying category, syntactic
category, partial algebra.

#### "Sublocales in formal topology"

Journal of Symbolic Logic **72 (2)** (2007) 463-482

ISSN: 0022-4812;
doi:10.2178/jsl/1185803619

Preprint version: pdf

The paper studies how the localic notion of sublocale transfers to formal topology. For any formal topology (not necessarily with positivity predicate) we define a sublocale to be a cover relation that includes that of the formal topology. The family of sublocales has set-indexed joins. For each set of base elements there are corresponding open and closed sublocales, boolean complements of each other. They generate a boolean algebra amongst the sublocales. In the case of an inductively generated formal topology, the collection of inductively generated sublocales has coframe structure.

Overt sublocales and weakly closed sublocales are described, and related via a new notion of "rest closed" sublocale to the binary positivity predicate. Overt, weakly closed sublocales of an inductively generated formal topology are in bijection with "lower powerpoints", arising from the impredicative theory of the lower powerlocale.

Compact sublocales and fitted sublocales are described. Compact fitted sublocales of an inductively generated formal topology are in bijection with "upper powerpoints", arising from the impredicative theory of the upper powerlocale.

#### "Some constructive roads to Tychonoff"

In: Laura Crosilla and Peter Schuster (eds.)
*From Sets and Types to Topology and Analysis:
Practicable Foundations for Constructive Mathematics*,
pp. 223 - 238. Oxford Logic Guides **48**,
Oxford University Press (2005).

ISBN: 0-19-856651-4. Click
here for more details.

Preprint version: pdf

The Tychonoff Theorem is discussed with respect to point-free topology, from the point of view of both topos-valid and predicative mathematics.

A new proof is given of the infinitary Tychonoff Theorem using predicative, choice-free methods for possibly undecidable index set. It yields a complete description of the finite basic covers of the product.

#### "A language for configuring multi-level specifications"

(Gillian Hill and Steven Vickers)

Final journal version appeared as:

Theoretical Computer Science **351**
(2006) 146 - 166

ISSN: 0304-3975;
doi:10.1016/j.tcs.2005.09.065

The preprint version is closer to the original conference
version, in:

Rattray, C., Maharaj, S. and Shankland, C. (eds)
*Algebraic Methodology and Software Technology*,
10th International Conference, AMAST 2004,
Stirling, Scotland, pp. 196-210. Springer Lecture Notes in Computer
Science 3116 (2004).

ISBN 3-540-22381-9

Preprint version: ps

This paper shows how systems can be built from their component parts with specified sharing. Its principle contribution is a modular language for configuring systems. A configuration is a description in the new language of how a system is constructed hierarchically from specifications of its component parts. Category theory has been used to represent the composition of specifications that share a component part by constructing colimits of diagrams. We reformulated this application of category theory to view both configured specifications and their diagrams as algebraic presentations of presheaves. The framework of presheaves leads naturally to a configuration lanaguage that expresses structuring from instances of specifications, and also incorporates a new notion of instance reduction from a particular configuration . The language now expresses the hierarchical structuring of multi-level configured specifications. The syntax is simple because it is independent of any specification language; structuring a diagram to represent a configuration is simple because there is no need to calculate a colimit; and combining specifications is simple because structuring is by configuration morphisms with no need to flatten either specifications or their diagrams to calculate colimits.

#### "Localic completion of generalized metric spaces II: Powerlocales"

(Steven Vickers)

Journal of Logic and Analysis **1(11)** (2009) pp. 1-48.

ISSN: 1759-9008;
doi:10.4115/jla.2009.1.11

Preprint version: pdf

(This paper is a greatly revised version of part of "Localic completion of quasimetric spaces".)

The work investigates the powerlocales (lower, upper, Vietoris) of localic completions of generalized metric spaces. The main result is that all three are localic completions of generalized metric powerspaces, on the Kuratowski finite powerset. This is a constructive, localic version of spatial results of Bonsangue et al. and of Edalat and Heckmann.

As applications, a localic completion is always open, and is compact iff its generalized metric space is totally bounded.

The representation is used to discuss closed intervals of the reals, with the localic Heine-Borel Theorem as a consequence.

The work is constructive in the topos-valid sense.

*Keywords:* locale, constructive, topos, metric, hyperspace, powerlocale.

*AMS Subject Code Classifications:* Primary -- 54B20. Secondary -- 06D22,
03G30, 54E50, 03F60.

#### "Localic completion of generalized metric spaces I"

(Steven Vickers)

Theory and Applications of Categories **14**
(2005), pp. 328-356.

ISSN: 1201-561X.

Free on-line at TAC: pdf

(This paper is a greatly revised version of part of "Localic completion of quasimetric spaces".)

We give a constructive localic
account of the completion of generalized metric spaces (gms's) in a
sense derived from that of Lawvere: a set *X*
equipped with a metric map from *X ^{2}* to the interval of
upper reals (approximated from above but not from below) from 0 to
infinity inclusive, and satisfying the zero self-distance law
and the triangle inequality. The completion is then a locale whose
points can be viewed either as Cauchy filters of formal balls or
(following Lawvere's approach using enriched categories) as flat left
modules.

Non-expansive functions between the gms's lift to continuous maps between the completions.

Various examples and constructions are given, including finite products.

The points of this completion are classically equivalent to those of the "Yoneda completion" of Bonsangue et al., modified to use Cauchy nets instead of sequences.

The exposition is constructive in the topos-valid sense and exploits the use of geometric reasoning to approach locales and toposes as "topology-free spaces".

#### "Entailment systems for stably locally compact locales"

(S.J. Vickers)

Theoretical Computer Science **316**
(2004) (special issue on Domain Theory) pp. 259-296.

ISSN: 0304-3975;
doi:10.1016/j.tcs.2004.01.033

The category $\mathbf{SCFr}_U$ of stably continuous
frames and preframe homomorphisms (preserving finite meets and directed
joins) is dual to the Karoubi envelope of a category
$\mathbf{Ent}$ whose objects are sets and whose
morphisms $X \rightarrow Y$ are upper closed relations between
the finite powersets $\mathcal{F}X$ and $\mathcal{F}Y$.
Composition of these morphisms is the "cut composition" of
Jung et al. that interfaces disjunction in the codomains with
conjunctions in the domains, and thereby relates to their *multi-lingual
sequent calculus*. Thus stably locally compact locales are
represented by "entailment systems" $(X,\vdash)$
in which $\vdash$, a generalization of entailment relations, is idempotent
for cut composition.

Some constructions on stably locally compact locales are represented in terms of entailment systems: products, duality and powerlocales.

Relational converse provides $\mathbf{Ent}$ with an involution, and this gives a simple treatment of the duality of stably locally compact locales. If $A$ and $ B$ are stably continuous frames, then the internal preframe hom $A \pitchfork B$ is isomorphic to $\hat{A} \otimes B$ where $\hat{A}$ is the Hofmann-Lawson dual.

For a stably locally compact locale $X$, the lower powerlocale of $X$ is shown to be the dual of the upper powerlocale of the dual of $X$.

#### "A universal characterization of the double powerlocale"

(S.J. Vickers + C.F. Townsend)

Theoretical Computer Science **316**
(2004) (special issue on Domain Theory) pp. 297-321.

ISSN: 0304-3975;
doi:10.1016/j.tcs.2004.01.034

Preprint version: pdf

The double powerlocale $\mathbb{P}(X)$ (found by composing, in either order, the upper and lower powerlocale constructions $P_U$ and $P_L$) is shown to be isomorphic in $[\mathbf{Loc}^{op}, \mathbf{Set}]$ to the double exponential $\mathbb{S}^{\mathbb{S}^X}$ where $\mathbb{S}$ is the Sierpinski locale. Further, $P_U(X)$ and $P_L(X)$ are shown to be the subobjects of $\mathbb{P}(X)$ comprising, respectively, the meet semilattice and join semilattice homomorphisms. A key lemma shows that, for any locales $X$ and $Y$, natural transformations from $\mathbb{S}^X$ (the presheaf $\mathbf{Loc}(- \times X, \mathbb{S})$) to $\mathbb{S}^Y$ (i.e. $\mathbf{Loc}(- \times Y, \mathbb{S})$) are equivalent to dcpo morphisms from the frame $\Omega(X)$ of $X$ to that of $Y$. It is also shown that $\mathbb{S}^X$ has a localic reflection in $[\mathbf{Loc}^{op}, \mathbf{Set}]$ whose frame is $\mathbf{dcpo}(\Omega(X), \Omega(Y))$.

The reasoning is constructive in the sense of topos validity.

#### "Compactness in locales and in formal topology"

(S.J. Vickers)

Annals of Pure and Applied Logic **137**
(2006), pp. 413-438. (Special issue for the Proceedings of the 2nd
Workshop on Formal Topology, Venice 2002.)

ISSN: 0168-0072;
doi:10.1016/j.apal.2005.05.028

Preprint version: pdf

If a locale is presented by a "flat site", it is shown how its frame can be presented by generators and relations as a dcpo. A necessary and sufficient condition is derived for compactness of the locale (and also for its openness). Although its derivation uses impredicative constructions, it is also shown predicatively using the inductive generation of formal topologies.

A predicative proof of the binary Tychonoff theorem is given, including a characterization of the finite covers of the product by basic opens. The discussion is then related to the double powerlocale.

#### "The double powerlocale and exponentiation: a case study in geometric logic"

(S.J. Vickers)

Theory and Applications of Categories **12** (2004) pp. 372-422

Free on-line at TAC: pdf

If $X$ is a locale, then its double powerlocale $\mathbb{P}(X)$ is defined to be $P_U(P_L(X))$ where $P_U$ and $P_L$ are the upper and lower powerlocale constructions. We prove various results relating it to exponentiation of locales, including the following. First, if $X$ is a locale for which the exponential $\mathbb{S}^X$ exists (where $\mathbb{S}$ is the Sierpinski locale), then $\mathbb{P}(X)$ is an exponential $\mathbb{S}^{\mathbb{S}^X}$. Second, if in addition $W$ is a locale for which $\mathbb{P}(W)$ is homeomorphic to $\mathbb{S}^X$, then $X$ is an exponential $\mathbb{S}^W$.

The work uses geometric reasoning, i.e. reasoning stable under pullback along geometric morphisms, and this enables the locales to be discussed using their points as though they were spaces. It relies on a number of geometricity results including those for locale presentations and for powerlocales.

#### "Localic sup-lattices and tropological systems"

(P. Resende + S.J. Vickers)

Theoretical Computer Science **305**
(2003) (special issue on Topology in Computer Science) pp. 311-346.

ISSN: 0304-3975;
doi:10.1016/S0304-3975(02)00702-8

The approach to process semantics using quantales and modules is
topologized by considering tropological systems whose sets of states
are
replaced by locales and which satisfy a suitable stability axiom. A
corresponding notion of localic sup-lattice (algebra for the lower
powerlocale monad) is described, and it is shown that there are
contravariant functors from sup-lattices to localic sup-latices and,
for
each quantale *Q*, from left *Q*-modules to localic right *Q*-modules.
A proof technique for third completeness due to Abramsky and
Vickers is reset constructively, and an example of application to
failures semantics is given.

#### "Presheaves as Configured Specifications"

(S.J.Vickers + G.A.Hill)

Formal Aspects of Computing **13** (2001) pp. 32-49.

ISSN: 0934-5043 (printed), 1433-299X (electronic);
doi:10.1007/PL00003938

Preprint version: ps

The paper addresses a notion of configuring systems, constructing them from specified component parts with specified sharing. This notion is independent of any underlying specification language and has been abstractly identified with the taking of colimits in category theory. Mathematically it is known that these can be expressed by presheaves and the present paper applies this idea to configuration.

We interpret the category theory informally as follows. Suppose *C* is
a category whose objects are interpreted as specifications, and for
which each morphism *u*: *X* -> *Y* is interpreted as contravariant
"instance reduction", reducing instances of specification *Y* to instances
of *X*. Then a presheaf *P* over *C* represents a collection of instances
that
is closed under reduction. We develop an algebraic account of
presheaves
in which we present configurations by generators (for components) and
relations (for shared reducts), and we outline a proposed configuration
language based on the techniques. Oriat uses diagrams to express
colimits of specifications, and we show that Oriat's category Diag(*C*)
of
finite diagrams is equivalent to the category of finitely presented
presheaves over *C*.

#### "Strongly Algebraic = SFP (Topically)"

Mathematical Structures in Computer Science**11**(2001) pp. 717-742.

ISSN 0960-1295; doi:10.1017/S0960129501003437

Certain "Finite Structure Conditions" on a geometric theory are shown to be sufficient for its classifying topos to be a presheaf topos. The conditions assert that every homomorphism from a finite structure of the theory to a model factors via a finite model, and they hold in cases where the finitely presentable models are all finite.

The conditions are shown to hold for the theory of strongly algebraic (or SFP) information systems and some variants, as well as for some other theories already known to be classified by presheaf toposes.

The work adheres to geometric constructivism throughout and in
consequence provides "topical" categories of domains
(internal in the category of toposes and geometric morphisms) with an
analogue of Plotkin's double characterization of strongly algebraic
domains, by sets of minimal upper bounds and by sequences of finite
posets.

#### "Localic Completion of Quasimetric Spaces"

Research Report DoC 97/2, Department of Computing, Imperial College
(1998).

(This has now been superseded by "Localic
completion of generalized metric spaces I" and "Localic
completion of generalized metric spaces II: Powerlocales".)

Preprint version: ps.gz

We give a constructive localic account of the completion of
quasimetric spaces. In the context of Lawvere's approach, using
enriched
categories, the points of the completion are flat left modules over the
quasimetric space. The completion is a triquotient surjective image of
a
space of Cauchy sequences and can also be embedded in a continuous
dcpo,
the "ball domain". Various examples and constructions are given,
including the upper, lower and Vietoris powerlocales, which are
completions of finite powerspaces. The exposition uses the language of
locales as "topology-free spaces".

#### "Topical Categories of Domains"

Mathematical Structures in Computer Science **9** (1999)
pp.569-616.

ISSN 0960-1295;
doi:10.1017/S0960129599002741

It is shown how many techniques of categorical domain theory can be expressed in the general context of topical categories (where "topical" means internal in the category Top of Grothendieck toposes with geometric morphisms). The underlying topos machinery is hidden by using a geometric form of constructive mathematics, which enables toposes as "generalized topological spaces" to be treated in a transparently spatial way, and also shows the constructivity of the arguments. The theory of strongly algebraic (SFP) domains is given as a case study in which the topical category is Cartesian closed.

Properties of local toposes and of lifting of toposes (sconing) are summarized, and it is shown that the category of toposes has a fixpoint object in the sense of Crole and Pitts. This is used to show that for a local topos, all endomaps have initial algebras, and this provides a general context in which to describe fixpoint constructions including the solution of domain equations involving constructors of mixed variance. Covariance with respect to embedding-projection pairs or adjunctions arises in a natural way.

The paper also provides a summary of constructive results concerning
Kuratowski finite sets, including a novel strong induction principle;
and shows that the topical categories of sets, finite sets and
decidable
sets are not Cartesian closed (unlike the cases of finite decidable
sets
and strongly algebraic domains).

#### "Topology via Constructive Logic"

Moss, Ginzburg and de Rijke (eds) "Logic, Language and Computation Vol
II" (Proceedings of conference on Information-Theoretic Approaches to
Logic, Language, and Computation, 1996). CSLI Publications, Stanford
(1999) pp. 336-345.

ISBN 1575861801; 157586181X

By working constructively in the sense of geometric logic, topology
can be hidden. This applies also to toposes as generalized topological
spaces.

#### "Toposes pour les vraiment nuls"

In : Edalat, Jourdan and McCusker (eds) "Theory and Formal Methods
1996", Third Imperial College Department of Computing Workshop on
Theory
and Formal Methods, April 1996, pp. 1-12. Imperial College Press,
London, 1996.

ISBN 1-86094-031-5

Restriction to geometric logic can enable one to define topological
structures and continuous maps without explicit reference to
topologies.
This idea is illustrated with some examples and used to explain toposes
as generalized topological spaces.

#### "Constructive points of powerlocales"

Mathematical Proceedings of the Cambridge Philosophical Society **122**
(1997), 207-222.

ISSN 0305-0041;
doi:10.1017/S0305004196001636

Results of Bunge and Funk and of Johnstone, providing constructively sound descriptions of the global points of the lower and upper powerlocales, are extended here to describe the generalized points and proved in a way that displays in a symmetric fashion two complementary treatments of frames: as suplattices and as preframes. We then also describe the points of the Vietoris powerlocale.

In each of two special cases, an exponential $^D ($ being the Sierpinski locale) is shown to be homeomorphic to a powerlocale: to the lower powerlocale when D is discrete, and to the upper powerlocale when D is compact regular.

#### "Toposes pour les nuls"

In: "Semantics Society Newsletter, Issue 4", 1995.Also available as Research Report DoC 96/4, Department of Computing, Imperial College (1996).

An introduction to Grothendieck's idea of toposes as generalized topological spaces.

Sheaves are described as continuous set-valued functions, geometric morphisms are described as continuous maps, and continuity itself is explained as "genericity + geometricity".

(K. Broda + S. Eisenbach + H. Khoshnevisan + S. Vickers)

Prentice Hall International Series in Computer Science (1994).

ISBN 0-13-098831-6

Downloadable version: pdf

Aimed at first or second year undergraduate students, *Reasoned
Programming* shows how to apply mathematical reasoning to the
development of the computer programs that users need, using logical
specifications to express these and then writing program code to
achieve
the objectives set out in the specifications.

The book starts with functional programming (including tutorial
material written for Miranda) for its simplicity, but also shows how it
can be used as a reasoning tool for imperative programming.

#### "Locales are not pointless"

In: Hankin, Mackie and Nagarajan (eds) "Theory and Formal Methods of
Computing 1994", 199-216, Imperial College Press.

ISBN 1-86094-003-X

Preprint version: ps, ps.gz, pdf

The Kripke-Joyal semantics is used to interpret the fragment of intuitionistic logic containing conjunction, implication, equality and universal quantification in the category of locales. An axiomatic theory is developed that can be interpreted soundly in two ways, using either lower or upper powerlocales, so that pairs of separate results can be proved as single formal theorems.

Openness and properness of maps between locales are characterized by descriptions using the logic, and it is proved that a locale is open iff its lower powerlocale has a greatest point. The entire account is constructive and holds for locales over any topos.

#### "Geometric logic as a specification language"

In: Hankin, Mackie and Nagarajan (eds) "Theory and Formal Methods of
Computing 1994", 321-340, Imperial College Press.

ISBN 1-86094-003-X

The "observational content" of geometric logic is discussed and it is proposed that geometric logic is an appropriate basis for a Z-like specification language in which schemas are used as geometric theory presentations.

A descriptional mechanism of "schema entailment", generalizing type constructions and logical entailment, is defined and investigated in some examples, and is also used in defining schema morphisms which are discussed briefly in connection with schema connectives, and with specifying and implementing operations.

#### "Towards a GeoZ toolkit"

(M. Dawson + S.J. Vickers)

In: Hankin, Mackie and Nagarajan (eds) "Theory and Formal Methods of
Computing 1994", Imperial College Press.

ISBN 1-86094-003-X

The use of Geometric Logic as the foundation of a specification language called GeoZ is proposed elsewhere. In this note we explore GeoZ from the perspective of practitioners, already familiar with the existing Z notation, by explaining the issues that arise and the role of schema entailment in the GeoZ reformulation of Z's mathematical toolkit.

#### "Geometric Logic in Computer Science"

pp. 37-54 in G.L. Burn, S.J. Gay and M.D. Ryan (eds) "Theory and Formal
Methods 1993", Proceedings of the first Imperial College Department of
Computing workshop on Theory and Formal Methods, Springer Workshops in
Computer Science, 1993.

ISBN 3-540-19842-3; 0-387-19842-3

Preprint version: ps.gz, ps, pdf

We present an introduction to geometric logic and the mathematical structures associated with it, such as categorical logic and toposes. We also describe some of its applications in computer science including its potential as a logic for specification languages.

#### "Quantales, Observational Logic and Process Semantics"

(S. Abramsky + S.J. Vickers)

pp.161-227 in Mathematical Structures in Computer Science vol. **3**
(1993).

doi:10.1017/S0960129500000189

Various notions of observing and testing processes are placed in a uniform algebraic framework in which observations are taken as constituting a quantale. General completeness criteria are stated, and proved in our applications.

NB - An earlier version of this paper was issued as a Departmental Report. The new version is substantially revised in its discussion and its mathematical techniques, though the overall approach is unchanged.

#### "Information Systems for Continuous Posets"

pp. 201-229 in "Theoretical Computer Science B" vol. **114**,
(1993)

ISSN 0304-3975;
doi:10.1016/0304-3975(93)90072-2

NB - This paper was previously entitled "Continuous Information Systems". It has been renamed to avoid confusion with Raymond Hoofman's paper.

The method of information systems is extended from algebraic posets to continuous posets by taking a set of tokens with an ordering that is transitive and interpolative but not necessarily reflexive. This develops results of Raney on completely distributive lattices and of Hoofman on continuous Scott domains, and also generalizes Smyth's "R-structures". Various constructions on continuous posets have neat descriptions in terms of these continuous information systems; here we describe Hoffmann-Lawson duality (which could not be done easily with R-structures) and Vietoris power locales. We also use the method to give a partial answer to a question of Johnstone's: in the context of continuous posets, Vietoris algebras are the same as localic semilattices.

#### "Geometric Theories and Databases"

pp. 288-314 in M.P. Fourman, P.T. Johnstone and A.M. Pitts (eds)
"Applications of Categories in Computer Science"
(Proceedings of the LMS Symposium, Durham 1991),
London Mathematical Society Lecture Note Series **177**,
Cambridge University Press, 1992.

ISBN 0-521-42726-6

Preprint version: pdf

Domain theoretic understanding of databases as elements of powerdomains is modified to allow multisets of records instead of sets. This is related to geometric theories and classifying toposes, and it is shown that algebraic base domains lead to algebraic categories of models in two cases analogous to the lower (Hoare) powerdomain and Gunter's mixed powerdomain.

#### "Preframe Presentations Present"

(P. Johnstone + S.J. Vickers)

pp. 193-212 in A. Carboni, M.C. Pedicchio and G. Rosolini (eds.)
Category Theory - Proceedings, Como 1990 (Springer Lecture Notes in
Mathematics **1488**,1991).

ISBN 3-540-54706-1; 0-387-54706-1;
doi:10.1007/BFb0084221

Preprint version: pdf

Preframes (directed complete posets with finite meets that distribute over the directed joins) are the algebras for an infinitary essentially algebraic theory, and can be presented by generators and relations. This result is combined with a general argument concerning categories of commutative monoids to give a very short proof of the localic Tychonoff Theorem. It is also shown how frames can be presented as preframes, a result analogous to Johnstone's construction of frames from sites, and an application is given.

#### "Formal Implementation"

Chapter = 25 in J.A. McDermid (ed.) The Software Engineer's
Reference Book, (Butterworth Scientific, London, 1991).

ISBN 0-750-61040-9

An account of the formal logic of pre- and post-conditions.

#### "Topology via Logic"

Cambridge Tracts in Theoretical Computer Science **5**
(Cambridge
University Press 1988).

ISBN 0-521-36062-5; 0-521-57651-2

An advanced textbook on topology for computer scientists with three unusual features. First, the introduction is from a localic 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 a substantial discussion of some computer science applications. Although books on topology aimed at mathematics exist, not book has been written specifically for computer scientists, and 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.

#### "A fixpoint construction of the *p*-adic
domain"

pp. 270-289 in D.H. Pitt, A. Poigne and D.E. Rydeheard, Category
Theory and Computer Science (Proceedings of Edinburgh Workshop, 1986)
(Springer Lecture Notes in Computer Science **283**, 1987).

ISBN 3-540-18508-9; 0-387-18508-9

The Kahn domain on *p* symbols can be given an arithmetic
structure so that its maximal elements are isomorphic to the *p*-adic
integers. This is described as a fixpoint of a functor in a category of
sheaves of rings.

#### "An algorithmic approach to the *p*-adic
integers"

pp. 599-616 in M. Main, A. Melton, M. Mislove and D. Schmidt
Mathematical Foundations of Programming Language Semantics (Proceedings
of Tulane Workshop, 1987) (Springer Lecture Notes in Computer Science **298**,
1988).

ISBN 3-540-19020-1; 0-387-19020-1

The ring of *p*-adic integers can be embedded as the maximal
elements in a Scott domain with algebraic structure. We show how
definitions and proofs in the mathematical theory of *p*-adics
can
be replaced by algorithms on the partial elements and formal
programming
methods working on the algorithms. Certain types of argumetns translate
naturally into non-deterministic algorithms using the Smyth power
domain.

#### "Theories as Categories"

(M.P. Fourman + S.J. Vickers)

pp. 434-448 in D. Pitt, S. Abramsky, A. Poigné and D. Rydeheard
(eds.) Category Theory and Computer Programming (Springer Lecture Notes
in Computer Science **240**, 1986).

ISBN 3-540-17162-2; 0-387-17162-2

This paper is not, and is not intended to be, original. Its purpose is to present a couple of examples from the folklore of topos theory, the theory of classifying topoi in particular. This theory and its applications spread initially without the benefit of widespread publication. Many ideas were spread among a relatively small group, largely by word of mouth. The result of this is that the literature does not provide an accessible introduction to the subject. Computer scientists studying the logic of computing have recently become interested in this area. They form our intended audience. In the space (and time) available we can only hope to provide a small selection of the many ideas missing from, or buried in, the literature. We attempt to give a perspective of the structure of the subject. Our selection is, of necessity, idiosyncratic, and our treatment brief. We hope that missing technical details may be reconstructed from the literature. This may require some diligence. [Yes, it did - SJV]

To apportion credit for the ideas presented here is difficult so long after the event. Lawvere and Joyal have a special position in htis subject. Their intuitions have shaped it. Many others, who participated in the Peripatetic Seminars in Europe, the New York Topos Theory Seminar (which also wandered) and the Category Theory meetings at Oberwohlfach, contributed also. Their contributions are, in general, better reflected in their published works. Finally, to apportion blame, this paper derives from notes taken by SJV of a talk by MPF. Any misrepresentations are the responsibility of the latter.