The meaning of the recursive type μt.t

Question

In the paper:

David B. MacQueen, Gordon D. Plotkin, Ravi Sethi: An Ideal Model for Recursive Polymorphic Types. Inf. Control. 71(1/2): 95-130 (1986).

the authors give a domain theoretic model for a large class of recursive types. More specifically, a large class of "well-behaved" types is defined (the so-called contractive ones) and their meaning is defined through the Banach fixpoint theorem.

As it turns out, a particularly simple recursive type that is not contractive, is the $\mu t.t$ one (which corresponds to the recursive type definition $t=t$). I was wondering, from a domain theoretic point of view, what should the meaning of this type be? One could say that its meaning is the trivial type (in the terminology of the above paper, the set that contains only the $\perp$ element). Alternatively, one could say that the meaning of the equation is the whole space of all possible values (denoted by V in the above paper). This second choice could be justified because the equation $t=t$ does not impose any restriction on the elements that satisfy it. Which of the two choices is the correct one?

Answer 1

$\mu$ denotes least fixed points, so $\mu t. t$ should be $\bot$, the initial/empty type (and $\nu t. t$ should be $\top$, the terminal/unit type).

Answer 2

The type equation $t = t$ does not restrict $t$ in any way. All types $t$ satisfy that equation. So, the least fixpoint is the least possible type $t$, that is, $\bot$, and the greatest fixpoint is the greatest possible type, that is, $\top$.