Re: [TYPES] Topology of the type T = T -> T

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]



On 30/11/14 22:05, Izaak Meckler wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Hi all,
>
> Does anyone know any resources describing the topology of the (say, Haskell
> 98) type given by
>
> data T = T (T -> T)
>
> This is something like the type of untyped lambda calculus programs. The
> topology I have in mind is defined as follows. A subset X of T is open set
> if there is a Haskell term
>
> f :: T -> ()
>
> with f x = () for x in A, and f x = undefined otherwise. The topology on T
> is the one generated by these open sets (generated in the classical sense,
> although I'd be interested also in the case where the unions are required
> to be definable functions out of Nat as described by Martin Escardo here
> <http://www.cs.bham.ac.uk/%7Emhe/papers/entcs87.pdf>, p. 33).
>
> It is not hard to show that T has non-trivial topology (for example, there
> are open sets separating the two church booleans) and it seems it's not
> compact. I'd appreciate any other info people have on this topology.

The references Guy gave you should help you to describe the topology
more explicitly.

Just one comment: the topology is compact, simply because there is a
bottom element in the domain.

The same is true for the type of integers: it is compact because it
has a bottom. What is not true for the type of integers is that the
total elements form a compact set (related to the Halting Problem).

You could ask whether the total elements of T form a compact set. But
we first have to agree what the total elements of T are/should be.

Back in 1997 in a domains workshop in Munich, Gordon Plotkin showed
that there is no reasonable notion of totality for such a domain, if I
remember correctly. But he didn't write this up, as far as I know.

Best wishes,
Martin