categories: preprints: Abstract Stone Duality papers

[Paul Taylor <pt@dcs.qmul.ac.uk>]

This is to invite your comments on

		  Sober Spaces and Continuations
		Subspaces in Abstract Stone Duality

			Paul Taylor

		http://www.dcs.qmul.ac.uk/~pt/ASD/

These two papers are, at last, complete and have been submitted to
a journal.  You can get them in various formats from this web address.

Together they develop the idea (that I first promoted in 1993) of a
category whose dual is monadic over the category itself. This was
inspired by Bob Pare's 1973 result for an elementary topos that the
contravariant powerset functor, which is self-adjoint, is monadic.
The category of locally compact sober spaces has the same property,
with the topology in place of the powerset.

Topological ideas, including compact Hausdorff and overt discrete
spaces, were developed in the paper
	Geometric and Higher Order Logic in terms of ASD
that appeared in TAC in December 2000.  That paper relied mainly 
on lattice-theoretic ideas, but "Sober Spaces..." is an introduction
to the impact of the monadic property on computation and topology.
(The Web page also has a non-technical "manifesto".)

"Sober Spaces..." actually discusses the weaker situation where the
dual category is a full subcategory of the category of algebras.
This happens exactly when every object is the equaliser of a certain
diagram that arises from the monad.  We call this property "sobriety",
although it is defined in terms of a (restricted) lambda-calculus
instead of lattice theory; the paper explains the connection between
the two.

The categorical construction that turns any category with an
exponentiating object Sigma into one in which all objects are sober
is essentially the same as that used by Thielecke, Fuhrmann and
Selinger to study continuations.  (However, ours makes little use
of Power and Robinson's notion of "premonoidal category".)

A corresponding "sober" lambda calculus is given.  Our new "focus"
operator is similar to the operator "force" that Thielecke et al.
discuss, except that its use is restricted to the situation where
there is NO computational effect, so it is denotational and does
not depend on an order of evaluation.

All powers of Sigma are automatically sober, so the only type in the
restricted lambda calculus that needs to be considered is N.  The
sober calculus is shown to be equivalent to adding a "description"
operator (a la Russell) to the restricted lambda calculus with
primitive recursion and the lattice operations.

The corollary of this is that any map $\Sigma^N\to\Sigma^U$ is a
homomorphism with respect to the monad iff it preserves finite meets
and the existential quantifier over N.  This is the base case in
showing that locale theory is captured by our lambda calculus.
The extension from N to arbitrary types depends on the fixed point
axiom, which is discussed (for the first time within ASD) in the
paper on domain theory that I have just started writing.

The introductory role of "Sober Spaces..." is concluded with
a brief explanation of how and why the calculus may be compiled
into pure PROLOG.


"Subspaces in ASD" completes the journey to the monadic situation.
It begins by explaining how the monadic property abstracts the 1930s
results of Stone, Tarski and Lindenbaum, and then how Beck's theorem
relates it to the subspace topology and injectivity of Sigma.

We say that $i:X\to Y$ is a "Sigma-split subspace" if "open subsets"
of X (maps $X\to\Sigma$) are expanded to open subsets of Y by means
of a morphism $I:\Sigma^X\to\Sigma^Y$.   As is remarked in the 
conclusion, this is really too strong.

The paper gives three constructions of the monadic completion of a
category.  The first formally adjoins Sigma-split equalisers in a way
similar to the Karoubi construction for splitting idempotents.  The
second is the opposite of the category of algebras, the crucial point
being the construction of coproducts of algebras; this is the result
that I had in 1993.

The third construction is a further extension of the sober lambda
calculus, now adding "subtypes" with a comprehension-like constructor.
The extra operator on terms, called "admit", plays a similar role
to "focus" in the sober calculus.   I presented preliminary results
about this calculus at the APPSEM meeting in Darmstadt in March 2001.

The comprehension calculus has a normalisation theorem, the
computational import of which is that  "i" and "admit" serve
only as compile-time type-annotations on terms, and may be
erased for execution.

The paper concludes with applications to coproducts (which clearly
exhibits the continuation-passing style) and to the quotient of
an overt discrete object by an open equivalence relation
(which was constructed in "Geometric and Higher Order Logic").

Paul Taylor
(no academic affiliation)