[Prev][Next][Index][Thread]

Fixed Points in Synthetic Domain Theory

Date: Mon, 1 Oct 90 19:12:57 BST

                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