Subject: categories: Synthetic Domain Theory

From: Paul Taylor <[email-masked]>
Date: Wed, 6 Jan 1999 17:52:25 GMT

As Jaap van Oosten says, I considered appropriate to mention the paper
"Axioms and (Counter)examples in Synthetic Domain Theory" by Alex Simpson
and himself when I announced my own draft paper "An Absract Stone Duality".

There are two reasons why I did consider this appropriate:
(1) they and I both use the heading "synthetic domain theory" for our
    work, and I feel that their work is important and should be considered
    alongside mine;
(2) people outside a particular discipline tend to go by the labels -
    "guilt by association" - so I was keen that those who had already
    looked at Jaap & Alex's paper (after they advertised it on "categories"
    before the holiday) should not assume that mine would be of the same kind.

I did not "polemicize" against it.  I said that I felt it was "arcane",
but wanted to say something positive about it first. Unfortunately, as
Alex has pointed out to me, I got the paper confused with our discussions
when I visited Edinburgh shortly before Jaap's announcement.

Jaap says that
> it is funny that our work, which builds on the tradition of turning
> SDT into an axiomatic theory (a process which I think is still unfinished),
> tradition which was started by Pino Rosolini, Wesley Phoa, Martin Hyland and
> Paul himself, is now found to be "arcane" (mind you, the whole subject is
> less than twenty years old) by Paul.

As a generality, and without wishing to take this argument any further,
surely a *founder* of a theory is qualified to describe a subsequent 
development of it as "arcane", ie accessible only to particular specialists,
and not what that founder had in mind?  SDT is a minority research topic,
still the plaything of a group of friends - that's what I like about it.
It's not Tony Blair's New Labour Party - we *are* allowed to disagree!

Anyway, since this particular beast has now been awoken from its slumbers,
I want to try to explain the mathematical content of this disagreement
briefly for a general audience.

Probably most "categories" readers have now heard the slogan,
	"Domains are sets - all functions are computable"
cf	"Manifolds are sets - all functions are smooth".
Synthetic domain theory and synthetic differential geometry are then about
(1) postulating conditions on the ambient topos (category of "sets")
(2) selecting from those "sets" those that are to be called "domains" or
    "manifolds" and
(3) using these ideas to prove interesting theorems or compute programs.

Much of the progress and disagreement in SDT has been about part (2).

Wesley Phoa, in his 1990 Cambridge thesis under Martin Hyland's supervision,
was the first to describe objects in a certain topos that looked like the
"domains" in theoretical computer science, rather than like lattices in
pure mathematics. (I *don't* mean to polemicize against Pino Rosolini there.)
Wes defined a certain preorder on each object of the topos, and restricted
to those objects for which this is a poset (antisymmetric), and further
to those for which it has directed joins, a least element and therefore
fixed points.

In particular, Wes selected his domains by testing each one for the relevant
infinitary condition.

My idea, in my 1991 LiCS paper, was that the infinitary condition could be
imposed on a *single* object, and the domains selected be means of a more
finitary categorical notion called "repleteness" that Martin Hyland had
introduced in his paper in the 1990 Como Category Theory proceedings.

Alex Simpson, John Longley and Jaap van Oosten later came up with another
infinitary condition, "well-completeness", and they, like Wes, select their
domains by testing this for each domain.  Under suitable conditions, this
gives a larger full subcategory than mine.

I do not dare even to give you the definition of well-completeness, let
alone attempt to defend or attack it.  You should read Alex and Jaap's
paper for that.

One of the objections to repleteness is that it is very difficult to 
characterise in familiar models.  Pino Rosolini has (with others)
investigated this, and you can find some of his results in the papers 
listed on his Hypatia page,
	http://hypatia.dcs.qmw.ac.uk/author/RosoliniG

(By the way, Hypatia now has a new server and some new code.  The machine
on which it was living from May to December 1998 was forever crashing,
partly because the mirrored papers were stored on a large collection of 
very old disks with a SCSI chain that made visitors to our machine room 
gasp in horror.)

My paper is, in this context, a defence of the notion of repleteness.
Since "attack is the best form of defence" it does this by replacing it
with a stronger notion, namely that a certain adjunction be monadic.
This has the effect of replacing the "domains" defined by ordered structures
that have been in use in theoretical computer science since the early 1970s
by locally compact locales.

Paul