7
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
1
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 2 '14 at 22:48
  • $\begingroup$ 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". $\endgroup$ – Marc Hamann Sep 3 '14 at 13:27
  • 1
    $\begingroup$ Sure, an example of that is the coalesced sum. $\endgroup$ – Andrej Bauer Sep 3 '14 at 17:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.