Fixed Points in Synthetic Domain Theory Carl Gunter's comments about the relationship between PERs and traditional semantics of programming languages has prompted me to make the announcement I meant to make a fortnight ago. I strongly differ from the Pennsylvanian point of view, though, in not considering PERs but an axiomatic approach, of which there are many different models. % TeX definitions \def\E{{\cal E}}\def\imp{\Rightarrow} \input mssymb % for the next two symbols only: \def\natno{{\Bbb N}}\def\sigleq{\sqsubseteq} My axiomatisation is as follows: $\E$ denotes an elementary topos with a natural numbers object $\natno$; by a "set" I mean an object of $\E$. If you don't like the word ``topos'', you can understand this as intuitionistic set theory. $\Sigma$ is a class of predicates (ie a subobject of $\Omega$) including true and false and closed under binary conjunction and countable (ie $\natno$-indexed) existential quantification (disjunction). This is required to satisfy the following two axioms: $$ \forall\sigma\in\Sigma.\lnot\lnot\Sigma\imp\Sigma $$ (Markov's principle) and $$ \forall\Phi:\Sigma^\natno\to\Sigma.\Phi(\lambda n.\top)\imp \exists n\in\natno.\Phi(\lambda m.m\leq n) $$ (finitary principle). The first will be assumed throughout, the second only when stated. Definitions: (i) the ($\Sigma$-pre-)order $x\sigleq y$ is defined by $\forall\phi\in\Sigma^X.\phi(x)\imp\Phi(y)$. (ii) an object $X$ for which this is antisymmetric is called a $\Sigma$-space; this is a ``pointwise Leibnitz principle''. (iii) A map $p:X\to Y$ which induces an isomorphism $\Sigma^Y\to\Sigma^X$ is called ($\Sigma$-)equable. (iv) An object $X$ such that any equable map $p:X\to Y$ with $Y$ a $\Sigma$-space is already an isomorphism is called ($\Sigma$-)replete; this is an ``objectwise Leibnitz principle''. (v) An object $X$ with a point $\bot$ such that $\forall\phi\in\Sigma^X.\phi(\bot)\imp\forall x\in X.\phi(x)$ is called focal. Then a predomain is a replete object and a domain is a focal replete object. Theorem 1 (i) The full subcategory of predomains is reflective and cartesian closed. (ii) The full subcategory of domains is cartesian closed. Theorem 2 The following are equivalent: (FPP) Every endofunction of a domain has a least fixed point. (DC) Every predomain is chain-complete and every map between predomains preserves suprema of chains. (LCC) For every chain of adjoint (or embedding-projection) pairs between predomains, the limit of the right adjoints (projections) is the colimit of the left adjoints (embeddings) (AX) the finitarity axiom holds. Powerdomains and dependent-type polymorphism can also be interpreted in this setting, but not impredicative (Girard-Reynolds second order) polymorphism. The Effective (Hyland) Topos, in which PERs are embedded, is a model. There are sheaf (Scott) models based on classical categories of domains. Indeed any small full subcategory of spaces (not necessarily T-zero) or locales may be used as a base category, so long as it includes Scott's $P\omega$ and if any space/locale $X$ is in it then so is $X\times P\omega$. There are even presheaf models, although the disjunctions in the axiomatisation have to be prefixed with $\lnot\lnot$ and the empty space must not be in the base category, but the two theorems still hold. The Recursive (Mulry) Topos is not a model of the axioms as they stand: the true natural numbers object has to be replaced with a recursive version. This is "work in progress" which was reported last week at the Categorical Logic in Computer Science workshop in Paris. Paul Taylor, Dept of Computing, Imperial College, London SW7 2BZ, UK pt@doc.ic.ac.uk +44 71 589 5111 x 5057 Subject: EECS '91 Preliminary Announcement EAST EUROPEAN CATEGORY SEMINAR March 12-18, 1991 (Tues. through Mon.) Predela, Bulgaria For details contact: Prof. V. Topencharov, Institute of Applied Mathematics and Computer Science Technical University of Sofia P.O. Box 384 Sofia 1000, Bulgaria Chartered bus from Sofia to Predala and back available free of charge. Accommodation included. The conference is held at a resort among beautiful mountains. This will be the sixth annual seminar. Extended abstracts (2 pages) are printed each year as proceedings of the seminar. For more information by e-mail, contact Fred Linton: FLINTON@EAGLE.WESLEYAN.EDU mentioning EECS '91.