Call-by-push-value's denotational semantics of "thunk diverge" 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.
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.