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

[XMATdb5r%DDATHD21.BITNET@MITVMA.MIT.EDU: Note for the TYPES mailing list]

Date:     Wed, 15 Jun 88 14:11:35 MEZ
From: XMATdb5r%DDATHD21.BITNET@MITVMA.MIT.EDU <Achim Jung>
Subject:  Note for the TYPES mailing list
To: meyer@theory.lcs.mit.edu

   The category of bifinite domains is not closed under the
       formation of dependent products.


In their recent paper "Domain Theoretic Models of Polymorphism", which
will appear shortly in Information and Computation, Coquand, Gunter
and Winskel (CGW) show how to use the class S of all (countably based)
Scott-domains as a model for the polymorphic lambda calculus. In this note
we want to point out that their construction does not work for the
class B of bifinite domains. (Which have been called SFP-objects,
strongly algebraic domains, profinite domains by others.)
To my knowledge this is the first example of a construction under
which the class of bifinites is not closed.

CGW interpret an impredicative type \Pi \alpha.\sigma as
the category of continuous sections of the Grothendieck fibration which
arises from a functor F:S^{EP} ---> S^{EP}. They show that for any
continuous functor F this category is isomorphic to a Scott-domain.

DEFINITION: Let C be a category of domains contained in B and let
F:C^{EP} ---> C^{EP} be a continuous functor. A continuous section
is a class of elements (t_X)_{X \in C} such that

(i)   t_X \in F(X).
(ii)  F(f)(t_X) \leq t_Y if f:X ---> Y is an embedding
(iii) t_{lim X_i} = \sup t_X_i for a directed system of domains.

Since F is continuous, any continuous section of F is determined by its
values on the finite posets contained in C. There are only set-many finite
posets up to isomorphism, so we can study the set
\Pi F = {(t_X)_{X\in C_fin} | F(f)(t_X) \leq t_Y for f:X ---> Y}
which CGW call the dependent product.

THEOREM (CGW): If F is a continuous functor from S^{EP} into
S^{EP}, then the dependent product \Pi F is a Scott-domain.

DEFINITION: A dcpo D with least element is an L-domain if every principal
ideal in D is a complete lattice.

In my thesis I have proved the following

THEOREM: If C is a cartesian closed category of algebraic dcpo's then
C is contained in the (cartesian closed) category of algebraic L-domains
or in the (cartesian closed) category of bifinite domains.

The proof is based on the following crucial

LEMMA: Let D and E be algebraic dcpo's with property m such that the
space [D ---> E] of Scott-continuous functions is algebraic. Then either
K(D) has property M or E is an L-domain.

(Reminder: property m = for each upper bound x of a set A there is a minimal
                        upper bound of A below x.
           property M = property m + each finite set has only finitely
                        many minimal upper bounds.
                 K(D) = the set of compact elements.)

EXAMPLE: The following is the smallest pointed poset which is not an
L-domain.

       o
      / \
  a  o   o b
     |\ /|
     |/ \|
  a' o   o b'       \bot < {a',b'} < {a,b} < \top
      \ /
       o

We call it NL.

We are now ready to give an example of a continuous functor
F:B^{EP} ---> B^{EP} for which the dependent product is not bifinite:

Let F map each object of B^{EP} onto NL and each morphism onto the
identity on NL.
Note that the set D of finite posets contained in B^{EP} (which are just
all finite pointed posets) can be ordered in the following way: X \leq Y
if there is an embedding from X to Y.
\Pi F has a particularly simple structure in this case:

\Pi F = { (t_X)_{X \in B_fin} | t_X \leq t_Y if X \leq Y},

and we see that \Pi F is nothing but [D ---> NL], the
space of monotone functions from D into NL. D itself is not a dcpo
but [D ---> NL] is isomorphic to [I(D) ---> NL], where I(D) denotes
the set of all ideals in D. By the Lemma cited above, K(I(D)) = D
should have property M, so it remains to show that this is not the case.

Indeed, U = \bot < {u_1,u_2} < {u_3,u_4} and
V = \bot < {v_1,v_2} < {v_3,v_4,v_5} have infinitely many minimal
upper bounds in D. These upper bounds can be thought of as the coalesced
sum of U and V plus n (where n > 3) minimal upper bounds of
{u_3,v_3}.
-----------------------------------
I am just about to write down the proofs in a detailed and selfcontained
form. Those who are interested to see more of the arguments can obtain
this note from me either by regular mail or by e-mail.


       Achim Jung
       Fachbereich Mathematik
       Technische Hochschule Darmstadt
       D-6100 Darmstadt
       West Germany
       e-mail: XMATDB5R@DDATHD21.BITNET