<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2014-09-02T22:48:13.217Z
Identifying all the least elements is a bit drastic. It would turn the predomain of natural numbers, which is flat, into a signleton. When turning a predomain into a domain we should seek an adjoint tothe forgetful functor. Lifting is such an adjoint.
Andrej Bauer
CC BY-SA 3.0
2014-09-03T13:27:05.733Z
That is the purpose of the qualifier: in general that won't make semantic sense.  I'm thinking of the instance where you build up your predomain from known chains, keeping their original bottoms. You turn this into a domain by "remembering" that all empty sets, divergent computations, etc. are the "same".
Marc Hamann
CC BY-SA 3.0
2014-09-03T17:11:41.093Z
Sure, an example of that is the coalesced sum.
Andrej Bauer
CC BY-SA 3.0
2014-09-02T19:53:24.263Z
2014-09-02T19:58:38.027Z
2014-09-02T19:58:38.027Z
Marc Hamann
<p>Yes, your reading is correct.</p>

<p>$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.</p>

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

<p>And yes, predomains need not have a least element.</p>

CC BY-SA 3.0
2014-09-02T22:46:28.300Z
2014-09-03T19:46:42.590Z
2014-09-03T19:46:42.590Z
Andrej Bauer
<p>I was reading about <a href="http://www.cs.bham.ac.uk/~pbl/papers/tlca99.pdf">Call-by-Push-Value</a> 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).</p>

<p>I was confused by the statement:</p>

<blockquote>
  <p>$[[ \mbox{thunk diverge} ]]\ \rho$ is the least element of the predomain $[[U\ \underline B]]\ \rho$</p>
</blockquote>

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

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

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

<p>Finally, predomains and domains are defined as:</p>

<blockquote>
  <p>A domain $(X, \le, \bot)$ is a predomain with a least element $\bot$.*</p>
</blockquote>

<p>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 <em>forgetting</em> 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$.</p>

<p><strong>Question</strong>: Is my new reading (above paragraph) correct?</p>

<p>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]]$). <strong>Does that make sense?</strong> 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".</p>

<p>*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:</p>

<blockquote>
  <p>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.</p>
</blockquote>

<pl.programming-languages><domain-theory>
Call-by-push-value's denotational semantics of "thunk diverge"
Blaisorblade
# Call-by-push-value's denotational semantics of "thunk diverge"

(Asked by: username_0 on 2014-09-02)

I was reading about [Call-by-Push-Value](http://www.cs.bham.ac.uk/~pbl/papers/tlca99.pdf) 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.

**Tags:** pl.programming-languages, domain-theory

---

## 2 answers

### Answer by username_2 on 2014-09-02. Score: 6 | Accepted answer

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 by username_1 on 2014-09-02. Score: 1

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.

> **Comments:**
> **username_2**: Identifying all the least elements is a bit drastic. It would turn the predomain of natural numbers, which is flat, into a signleton. When turning a predomain into a domain we should seek an adjoint tothe forgetful functor. Lifting is such an adjoint.  
> **username_1**: That is the purpose of the qualifier: in general that won't make semantic sense.  I'm thinking of the instance where you build up your predomain from known chains, keeping their original bottoms. You turn this into a domain by "remembering" that all empty sets, divergent computations, etc. are the "same".  
> **username_2**: Sure, an example of that is the coalesced sum.  

---

