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.
Call-by-push-value's denotational semantics of thunk diverge
pl.programming languages;domain theory
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.