Subject: categories: synthetic topology

From: Martin Escardo <[email-masked]>
Date: Fri, 4 Jun 2004 13:57:46 +0100

This is to advertise the monograph

        "Synthetic topology of data types and classical spaces"

    http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf (or dvi or ps)

which will appear soon in volume 83 of ENTCS.

NB. (1) For those of you who attended my PSSL talk in Cambridge: The
topos-theoretic treatment of synthetic topology has not been included
here. (2) This monograph supersedes a preliminary version which was
previously available from my web page.

Martin Escardo
--

Summary (not as in the monograph)

This monograph consists of three parts divided in 6+5+2 chapters.

Part II (topology of classical spaces) applies the exponential law for
function spaces, with the aid of the Sierpinski space, to develop the
core of classical topology in a transparent (and constructive)
way. Mathematicians can start from this part, and even confine their
attention to it.

Part I (topology of data types) emulates the second and stands on its
own. It starts from the well known ideas that (1) the Sierpinski space
plays the role a data type of results of semidecisions or
observations, and (2) the notion of continuous map has that of
computable or programmable map as a computational counterpart. The
development of the synthetic topology of data types offered in this
part is operational rather than denotational. This is to emphasize
that the topology is there, even in the case of sequential programming
languages, independently of which denotational model one favours (if
any).

Part III starts by unifying the first and the second, again following
well known ideas, and then develops further applications to
computation, this time with the aid of denotational semantics.  In
particular, the Tychonoff theorem for countably many factors is
invoked to establish termination of a certain program (in the
simply-typed lambda calculus with natural numbers and fixed-point
recursion). In turn, termination of the program implies the Tychonoff
theorem for countably many second countable compact spaces.
------------------------------------------------------------------------
http://www.cs.bham.ac.uk/~mhe/papers/entcs87.pdf
------------------------------------------------------------------------