Call-by-push-value's denotational semantics of "thunk diverge"

Question

I was reading about Call-by-Push-Value in the introducing paper from 1999, but I have some confusion, partially because of my unfamiliarity with domain theory. I might have figured it out, but I'd hope to get it confirmed. (If this is not the appropriate venue, advise is welcome on which one is).

I was confused by the statement:

$[[ \mbox{thunk diverge} ]]\ \rho$ is the least element of the predomain $[[U\ \underline B]]\ \rho$

I was confused because AFAICS, predomains are not guaranteed to have a bottom element in general.

The behavior of $[[U\ \underline B]]$ was defined earlier by saying:

if $[[\underline B]]$ is the domain $(X, \le, \bot)$, then $[[U\ \underline B]]$ is its underlying predomain $(X, \le)$

Finally, predomains and domains are defined as:

A domain $(X, \le, \bot)$ is a predomain with a least element $\bot$.*

Originally, I misunderstood the text as implying that to construct $[[U\ \underline B]]$, you remove the bottom element from $[[\underline B]]$. Now, instead, I realize that probably, the semantics of U is just forgetting that $\bot$ is a distinguished element (like a forgetful functor from the category of domains to category of predomains, if my intuition is right). That's because, in a domain, we assume that $\bot$ belongs to X, not to its lifting: that is, $\bot \in X$, instead of $\bot \in X_\bot$.

Question: Is my new reading (above paragraph) correct?

Furthermore, the paper seems to imply that $[[U (F A)]]$ is a predomain created by lifting $[[A]]$ (by adding an additional bottom element below all elements of $[[A]]$). Does that make sense? If so, $T = U \circ F$ would seem to be a partiality monad, matching the fact that this definitions are needed to support the "divergence side effect".

*The definition of predomain is longer, but apparently it does indeed not imply the existence of least elements, so it should be irrelevant to the question. For reference:

A predomain $(X, \le)$ is a countably based, algebraic directed-complete poset, with joins of all nonempty bounded subsets, in which the down-set $\{y \in X : y \le x\}$ of each $x \in X$ has a least element.

Answer 1

Yes, your reading is correct.

$U$ forgets that something is a domain, but does not change the underlying carrier set or the poset structure. The least element is still there.

It is also the case that $U \circ F$ can be equipped with the structure of a monad, as you say.

And yes, predomains need not have a least element.

Answer 2

That definition implies that there is no required unique bottom in a predomain, i.e. each down set (reverse chain) could have a distinct least element, but that there is no necessary least element for the whole structure.

You could form a domain by appending a bottom under all other least elements, or by identifying all least elements (i.e. say they are all the same element) if that is semantically viable in your structure.