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) 23-Jan-2002 15:09:12 -0400,1835;000000000000-00000000