Abstract Stone Duality update

Abstract Stone Duality update

[Paul Taylor]

Abstract Stone Duality is a reaxiomatisation of general topology that
is intended to unify it with recursion theory and translate topological
constructions into executable programs.  In a sense, it turns denotational
semantics on its head: from topology (not just domain theory) to programs.
The underlying idea is Pare's theorem, that the category of "frames" is
both dual to and monadic over the category of "spaces".

The leading concrete examples are
 * the category of locally compact locales and
 * any elementary topos,
so - unlike existing programming languages and formal type theories -
there are "subtypes",  which can be carved out by means of something
like the axiom of comprehension in set theory.

Unfortunately the subject is not yet in a state where I can give an
introduction suitable for either topologists or computer scientists:
I am still building basic categorical structure on the central
hypothesis, and familiarity with Beck's theorem that characterises
monadic adjunction is essential at this stage.

This is just an interim progress report for those that already know
a little about this work.   Links to the published and draft papers are
at	http://www.dcs.qmw.ac.uk/~pt/ASD
or	http://hypatia.dcs.qmw.ac.uk/author/TaylorP

In particular, the paper that I presented at CT2000 in Como,
        Non-Artin Gluing in Recursion Theory and
        Lifting in Abstract Stone Duality
recently came back from the referees and has now been revised.

If you have any comments on this paper, please tell me now so that
they can be incorporated in the revised version.

It contains a counterexample to show that the Artin comma square for
recovering the topology on a space from the topologies of an open subspace
and its closed complement does not work for the analogous lattices of
recursively enumerable subsets of N, considered as Godel numbers for
terminating and non-terminating programs.

However, it analyses the gluing problem a little further, and shows that
the modular law for lattices plays an important part.   On this is built
the construction of the partial map classifier in abstract Stone duality.

The paper follows and relies heavily on
        Geometric and Higher Order Logic in Abstract Stone Duality,
which was published in Theory and Applications of Categories in Dec 2000.

For the past few months I have been working on (the category theory and)
a lambda calculus for the monadic principle that underlies ASD.  This was
presented at the APPSEM workshop in Darmstadt in March.   I was hoping
to have it in a releasable state by now, but, as usual, the paper grew
much too big, so I split it in two, so it lost its narrative structure.
I hope to be able to release a draft of that later in the summer.

The main job for the summer is to get working a prototype compiler that
I started writing last summer, to translate from my comprehension-like
lambda calculus into pure PROLOG.   The reason for choosing PROLOG is 
that its semantics is (amongst existing programming languages) closest
to the semantic ideas in ASD.

Paul