Interesting posting on McGill category group from Paul Taylor
Wed Jun 20 23:13:02 2001
Abstract Stone Duality is a reaxiomatisation of
general topology that
is intended to unify it with recursion theory and
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
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
I am still building basic categorical structure on the
hypothesis, and familiarity with Beck's theorem that
monadic adjunction is essential at this stage.
This is just an interim progress report for those that
a little about this work. Links to the published and
draft papers are
In particular, the paper that I presented at CT2000 in
Non-Artin Gluing in Recursion Theory and
Lifting in Abstract Stone Duality
recently came back from the referees and has now been
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
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
I hope to be able to release a draft of that later in
The main job for the summer is to get working a
prototype compiler that
I started writing last summer, to translate from my
lambda calculus into pure PROLOG. The reason for
choosing PROLOG is
that its semantics is (amongst existing programming
to the semantic ideas in ASD.
Do You Yahoo!?
Get personalized email addresses from Yahoo! Mail