#
Sober spaces and continuations

##
Paul Taylor

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, Fuhrmann 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 $\lambda$-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.

Keywords: observable type; predicate transformer; continuation passing style; sober space;
locally compact space; locally quasi-compact space; locale; prime filter; Sierpinski space;
schizophrenic object; Stone duality; strong monad; Kleisli category; premonoidal category;
prime lambda term; sober lambda calculus; theory of descriptions; general recursive function.

2000 MSC: 06D22, 06E15, 18B30, 18C20, 18C50, 22A26, 54A05,
54C35, 54D10, 54D45.

*Theory and Applications of Categories*, Vol. 10, 2002, No. 12, pp 248-300.

http://www.tac.mta.ca/tac/volumes/10/12/10-12.dvi

http://www.tac.mta.ca/tac/volumes/10/12/10-12.ps

http://www.tac.mta.ca/tac/volumes/10/12/10-12.pdf

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/10/12/10-12.dvi

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/10/12/10-12.ps

TAC Home