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

Effective topological lambda models


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

The aim of this note is to point out that a result in a paper of mine
which just appeared in Information and Computation (Vol. 122, No. 1,
pp.  120--139, Corollary 3.4) has some consequences on the
nonexistence of effective topological non-domain lambda models.


In that paper effectively given spaces are considered.

Def.1. A T_0 space X is "effectively given" if (1) and (2) hold:

(1) X has a countable basis {B_n | n \in Nat}.

(2) On this basis a strong inclusion relation \prec is defined such
    {(n,m) | B_n \prec B_m} is effectiveley enumerable.


Here \prec is a "strong inclusion" if from B_n \prec B_m it follows
that B_n \subseteq B_m. So one can also choose \prec to be normal set
inclusion.  Whether one does this depends on the condition (3) in
Def. 3.


Def. 2. An object X in a ccc of topological spaces is a "lambda model"
if there is a surjection p: X -> [X -> X] and maps

    \psi: \Lambda(C) ->> X in SET, and

    \phi: (\Lambda(C),\circ) -> ([X -> X],\circ) in MONOID

such that \phi = p \circ \psi and \phi(M)(\psi(N)) = \psi(MN).

(Here \Lambda(C) is the set of all lambda terms with constants in C
modulo \alpha conversion.)


Def. 3. A topological lambda model X is "effectively given" if (1) -
(3) hold:

(1) X is effectively given.

(2) One can effectively list all pairs (t,n) where t is a lambda term and
    n \in Nat such that \psi([t]) \in B_n. (Here [t] is the element of
    \Lambda(C) generated by t.)

(3) There is an effective procedure such that (a) and (b) hold:

   (a) For any effective sequence (B_m) which is decreasing with respect
       to \prec and the filter generated by which is the neighbourhood
       filter of a point in \psi(\Lambda(C) the procedure computes a
       lambda term t such that \psi([t]) is that point,

   (b) If for any effective sequence (B_m) the procedure converges to a
       lambda term t, then the collection of all sets B_m is a base of the
       neighbourhood filter of \psi([t]).


As a consequence of the result mentioned above one obtains:

Theorem. Let X be an effectively given lambda model. Then for each
point in \psi(\Lambda(C)) there is a finite element of
\psi(\Lambda(C)) below it (with respect to the specialization order).

Here an element is called "finite" if its neighbourhood filter is
principal (i.e., if the set of all points above it is open).


Applications:

1. Let X = \psi(\Lambda(C)). Then X cannot be T_1.

Proof. Suppose X is T_1 one. Then the specialization order coincides
with identity. By the theorem it follows that the topology is the
discrete one.  This implies that [X->X] = X^X, which is impossible by
Cantor's theorem since [X->X] is a retract of X.


2. Suppose each map f:\psi(\Lambda(C)) -> \psi(\Lambda(C)) has a
continuous extension F:X -> X. Then X cannot be T_1.


3. X cannot be T_1 and compact.



Dieter Spreen