Sober spaces and continuations

Paul Taylor

Theory and applications of categories, Tome 10 (2002), pp. 248-300.

Résumé

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.

Détail

Classification : 06D22, 06E15, 18B30, 18C20, 18C50, 22A26, 54A05, 54C35, 54D10, 54D45.
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.