Interesting posting on McGill category group from Paul Taylor

[Galchin Vasili]

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




__________________________________________________
Do You Yahoo!?
Get personalized email addresses from Yahoo! Mail
http://personal.mail.yahoo.com/