Sober Spaces and Continuations

Paul Taylor

This is the first paper in the core theory of Abstract Stone Duality for locally compact spaces. It was published in Theory and Applications of Categories 10(12) 248–299 in July 2002 (BibTeX).


A topological space is sober if it has exactly the points that are dictated by its open sets. We explain the analogy with the way in which computational values are determined by the observations that can be made of them. A new definition of sobriety is formulated in terms of lambda calculus and elementary category theory, with no reference to lattice structure, but, for topological spaces, this coincides with the standard lattice-theoretic definition. The primitive symbolic and categorical structures are extended to make their types sober. For the natural numbers, the additional structure provides definition by description and general recursion.

We use the same basic categorical construction that Thielecke, Führmann and Selinger use to study continuations, but our emphasis is completely different: we concentrate on the fragment of their calculus that excludes computational effects, but show how it nevertheless defines new denotational values. Nor is this “denotational semantics of continuations using sober spaces”, though that could easily be derived.

On the contrary, this paper provides the underlying λ-calculus on the basis of which abstract Stone duality will re-axiomatise general topology. The leading model of the new axioms is the category of locally compact locales and continuous maps.


Postscript: The analogue of the connection between sobriety and definition by description for ℕ is Dedekind completeness for ℝ.



Acknowledgements

I would like to thank Carsten Führmann, Ivor Grattan-Guiness, Peter Johnstone, Peter Landin, Andy Pitts, John Power, Pino Rosolini, Phil Scott, Hayo Thielecke, Steve Vickers, Graham White, Claus-Peter Wirth and Hongseok Yang for their helpful comments on this paper.

BibTeX entry

   @article{TaylorP:sobsc,
      author    = {Taylor, Paul},
      title     = {Sober Spaces and Continuations},
      journal   = {Theory and Applications of Categories},
      publisher = {Mount Allison University},
      year      = 2002, month = {July},
      volume    = 10, number = 12, pages = {248--299},
      url       = {PaulTaylor.EU/ASD/sobsc},
      amsclass  = {06D22, 06E15, 18B30, 18C50,
                   22A26, 54C35, 54D10, 54D45}}

Download the paper to print it

PDF,  DVI,  compressed PostScript  or  A5 booklet.




Table of contents


1. Computational values


2. The restricted λ-calculus


3. Algebras and homomorphisms


4. Sobriety and monadicity


5. Topology revisited


6. Enforcing sobriety


7. The structure of SC


8. A lambda calculus for sobriety


9. Theory of descriptions


10. Sobriety and description


11. Directions


References

This document was translated from LATEX by HEVEA.