<p>This is only half an answer, but allow me to clear up a constructive point about the interval domain.</p>
<p>The usual definition of the interval domain is
<span class="math-container">$$\mathrm{I}\mathbb{R} = \{[a,b] \mid a, b \in \mathbb{R} \land a \leq b \} \cup \{\mathbb{R}\},
$$</span>
ordered by reverse inclusion. If we try to use this definition constructively, we get stuck when showing that it is a dcpo. Even showng that an increasing sequence has a supremum is impossible (because constructively it may not be the case that a bounded increasing sequence of reals has a supremum).</p>
<p>The correct constructive definition of the interval domain goes as follows. An element of <span class="math-container">$\mathrm{I}\mathbb{R}$</span> is a pair <span class="math-container">$(L, U) \in P(\mathbb{Q}) \times P(\mathbb{Q})$</span> such that</p>
<ol>
<li><span class="math-container">$L$</span> is lower and rounded: <span class="math-container">$p \in L \iff \exists q \in L \,.\, p &lt; q$</span>.</li>
<li><span class="math-container">$U$</span> is upper and rounded: <span class="math-container">$q \in U \iff \exists p \in U \,.\, p &lt; q$</span>.</li>
<li><span class="math-container">$L$</span> and <span class="math-container">$U$</span> are disjoint.</li>
</ol>
<p>The ordering is defined by
<span class="math-container">$$
(L,U) \sqsubseteq (L', U')
\iff
L \subseteq L' \land U \subseteq U'.
$$</span>
Think of <span class="math-container">$L$</span> and <span class="math-container">$U$</span> as the endpoints of the interval, given respectively as a lower and an upper Dedekind cut. Note that <span class="math-container">$\emptyset$</span> is allowed as a cut. It represents either <span class="math-container">$-\infty$</span> or <span class="math-container">$\infty$</span>, for instance <span class="math-container">$(\emptyset, \emptyset)$</span> is the bottom element, <span class="math-container">$(\emptyset, U)$</span> represents an interval <span class="math-container">$(-\infty, u]$</span>, and <span class="math-container">$(L, \emptyset)$</span> represents an interval <span class="math-container">$[\ell, \infty)$</span>.</p>
<p>Clearly, we have an inclusion <span class="math-container">$\mathrm{I}\mathbb{R} \subseteq P(\mathbb{Q}) \times P(\mathbb{Q})$</span>, and since
<span class="math-container">$$
P(\mathbb{Q}) \times P(\mathbb{Q}) \cong
P(\mathbb{Q} + \mathbb{Q}) \cong
P(\omega),
$$</span>
we have an inclusion <span class="math-container">$\mathrm{I}\mathbb{R} \to P(\omega)$</span>. The other direction I am still thinking about.</p>
<p>It is also quite clear that the two domains are not isomorphic posets, as <span class="math-container">$P(\omega)$</span> is an algebraic lattice but <span class="math-container">$\mathrm{I}\mathbb{R}$</span> is not.</p>
<p><strong>Supplemental:</strong> I cannot tell from your question what precisely you are trying to do, but perhaps you will find <a href="https://doi.org/10.1016/j.tcs.2014.02.042" rel="nofollow noreferrer">Cartesian closed categories of separable Scott domains</a> relevant. There we find invariants, namely <em>coherence numbers</em>, that determine when one universal domain embeds into another.</p>

CC BY-SA 4.0
2021-11-07T07:57:22.277Z
Thanks. Okay, I see your point that the computable subset of $\mathbf{I}\mathbb{R}$ won't be a subdomain (i.e., the "whether or not" part of my comment above should just be "not"). And thanks also for the more formal analysis than anything that had come to mind for me. It all makes me realize that I should have omitted "constructive" in the original question (I should maybe just be interested in the computable elements of each domain, and maybe an isomorphism between those subsets).
John Forkosh
CC BY-SA 4.0
2021-11-07T08:47:42.157Z
That won't work either. The computable elements form *effective* domains (you get the c.e. sets instead of $P(\omega)$ and the computble interval domain). These are not computably isomorphic as domains because, again, one is algebraic and the other is not.
Andrej Bauer
CC BY-SA 4.0
2021-11-07T08:48:00.853Z
Do you have an idea that any two universal domains ought to be isomorphic? Because that is not true.
Andrej Bauer
CC BY-SA 4.0
2021-11-07T09:23:12.860Z
I linked to a paper that classifies universal separable Scott domains up to retraction, perhaps that will be relevant to your work.
Andrej Bauer
CC BY-SA 4.0
2021-11-08T06:04:52.553Z
Re "idea that any two universal domains ought to be isomorphic": isomorphic is apparently too strong, but what had crossed my mind is that given any two universal domains $\mathcal{U}_1$ and $\mathcal{U}_2$, and any domain $D$, then there always exist retractions $\hat{r}_1:\mathcal{U}_1\to D$ and $\hat{r}_2:\mathcal{U}_2\to D$. So we can always say $\hat{r}_1\sim\hat{r}_2$ in some way, whereby the two collections of retractions are related in some way, hopefully a strong way, which hopefully extends to $\mathcal{U}_1$ and $\mathcal{U}_2$ themselves. But I hadn't carried this idea any further.
John Forkosh
CC BY-SA 4.0
2021-11-08T06:12:08.057Z
Re "link to ccc's of separable Scott domains": Thanks for the link. Have only just briefly scanned it so far, and looks very interesting, so I'll be taking a deeper dive. And re "relevant to your work", maybe "work" is too strong a word. I'm only just self-studying all this stuff. The question/idea wasn't intended to be "research level", per se. But this group seems to be the only computer science group with a "domain theory" tag.
John Forkosh
CC BY-SA 4.0
2021-11-08T13:25:33.037Z
If a an object $U$ is universal in the sense that there is a retraction $X \to U$ from every other object, then of course, given any two universal objects there will be retractions between them. Moreover, if we let $R(X)$ be the poset of retracts of $X$, then for universal objects $U_1$ and $U_2$, the posets $R(U_1)$ and $R(U_2)$ are equivalent. For sufficiently nice notion of domain and "retract", it may even happen that $R(X)$ is itself a domain, in which case we can say even more.
Andrej Bauer
CC BY-SA 4.0
2021-11-06T10:10:13.937Z
2021-11-07T09:22:23.503Z
2021-11-07T09:22:23.503Z
Andrej Bauer
<p>Is there a constructive way to one-to-one associate elements <span class="math-container">$x\in\mathcal{P}\omega$</span> with elements <span class="math-container">${\scriptstyle\mathbf I}\in\mathbf{I}\mathbb{R}$</span> ?<br>
I assumed there should be since they're both universal (so kind of an embedding-embedding pair, so to speak), but haven't been able to figure out how it could be done, nor google a solution.<br></p>
<p><b>Edit:</b> Re comment How do you constructively embed <span class="math-container">$\mathcal{P}(\{0,1,2\})$</span> into the interval domain?...<br>
    Well, here's what I'd been thinking to do for <span class="math-container">$\mathcal{P}\omega$</span> in general, which doesn't work as a bijection, but which maybe vaguely works as an embedding. It's all kind of fast-and-loose in the spirit of Stoy's remark about &quot;fiddling with sets of integers&quot; (last paragraph on pg.116 in his book).<br>
    First let's consider your definition <span class="math-container">$\mathbf{I}\mathbb{R} = \{[a,b] \mid a, b \in \mathbb{R}_{[0,1]} \land a \leq b \}$</span> restricted to <span class="math-container">$\mathbb{R}_{[0,1]}=\{r\in\mathbb{R}\mid 0\leq r\leq1\}$</span>. Then for <span class="math-container">$x\in\mathcal{P}\omega$</span>, first, for each <span class="math-container">$i\in x$</span>, use the <b>inverse</b> pairing function <span class="math-container">$\mathbb{N}\times\mathbb{N}\to\mathbb{N}$</span>, e.g., <a href="https://en.wikipedia.org/wiki/Pairing_function" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/Pairing_function</a>, to get <span class="math-container">$x\to x_1,x_2$</span>. Now use the usual construction <span class="math-container">$x\subseteq\mathbb{N}\to r_x=\sum_{i\in x}\frac1{2^i}\in\mathbb{R}_{[0,1]}$</span>. So now we have <span class="math-container">$x\in\mathcal{P}\omega\to r_{x_1},r_{x_2}$</span>, with which we associate the interval <span class="math-container">$[r_{_\mbox{lo}},r_{_\mbox{hi}}]$</span>, choosing the lesser of <span class="math-container">$r_{x_1},r_{x_2}$</span> for <span class="math-container">$r_{_\mbox{lo}}$</span> and ditto for hi. And those <span class="math-container">$r$</span>'s will be rational if <span class="math-container">$x$</span> is finite, and computable/constructive if it's r.e.<br>
    Second, if it's really necessary to consider <span class="math-container">$\mathbb{R}$</span> rather than just <span class="math-container">$\mathbb{R}_{[0,1]}$</span>, then for any <span class="math-container">$x\in\mathcal{P}\omega$</span>, first get <span class="math-container">$x_1,x_2$</span> as above, but now separate each into its even and odd numbers, i.e., <span class="math-container">$x_1^e=\{\frac i2\mid i\in x_1\land i\mbox{ even}\}$</span> and <span class="math-container">$x_1^o=\{\frac{i+1}2\in x_1\mid i\mbox{ odd}\}$</span>. And now use <span class="math-container">$x_1^e$</span> to determine the integer part of <span class="math-container">$r_{x_1}$</span> as <span class="math-container">$\sum_{i\in x_1^e}2^i$</span>, and use <span class="math-container">$x_1^o$</span> to determine the decimal part as above.<br>
   </p>

CC BY-SA 4.0
2021-11-05T13:02:08.343Z
Is this supposed to be an isomorphism of underlying sets (any bijection), or an isomorphism of posets (monotone), or an isomorphism of domains (continuous)?
Andrej Bauer
CC BY-SA 4.0
2021-11-05T14:25:28.917Z
Sorry, I misread, you're looking for embeddings, not isomorphisms.
Andrej Bauer
CC BY-SA 4.0
2021-11-05T14:55:07.173Z
Can you embed $P(\{0,1,2\})$ into $\mathrm{I}\mathbb{R}$? Also, please write down the exact definition of $\mathrm{I}\mathbb{R}$.
Andrej Bauer
CC BY-SA 4.0
2021-11-06T06:42:07.787Z
@AndrejBauer Thanks for your several comments. Actually, I was looking for an isomorphism, not just into as implied by "embedding", but also onto (as would have been implied by "projection"). Continuous if possible, but I haven't even been able to construct any bijection, so basically just looking for any ideas. Re $\mathcal{P}(\{0,1,2\})$, of course I can brute-force embed that small set into just about anything, but I'm not seeing any "systematic" way to do it that would extend to $\mathcal{P}\omega$. As for the definition, yeah I've seen several. Choose any you like (continued below...)
John Forkosh
CC BY-SA 4.0
2021-11-06T06:53:16.230Z
@AndrejBauer (...continued from above) that permits construction of a bijection. I've personally been mostly trying to use Chapter 7 of Stoltenberg-Hansen, et al, https://books.google.com/books/about/?id=epb39s2wgt0C But, e.g., http://www.entcs.org/mislove/oxford06.pdf is fine if it more easily permits construction of a bijection. Again...just looking for ideas how it might be done.
John Forkosh
CC BY-SA 4.0
2021-11-06T08:30:42.683Z
Really? How do you **constructively** embed $P(\{0,1,2\})$ into the interval domain? And I think it's still important that you write down what you think the constructive interval domain is. Do you use Cauchy reals, Dedekind reals, or lower and upper Dedekind cuts? It may matter.
Andrej Bauer
CC BY-SA 4.0
2021-11-07T07:40:11.380Z
@AndrejBauer Re "Really?..." above. I edited the question to illustrate what I'd been very loosely playing around with for $\mathcal{P}\omega$. And with respect to that, I suppose that the interval domain is what you said in your answer, and its constructive elements are those intervals whose lower,upper bounds are computable reals (whether or not that subset actually comprises a subdomain isn't immediately clear to me).
John Forkosh
CC BY-SA 4.0
2021-11-07T08:49:26.553Z
Your edit is not using $\mathcal{P}(\omega)$ but $2^{\mathbb{N}}$.
Andrej Bauer
CC BY-SA 4.0
2021-11-08T06:18:17.680Z
@AndrejBauer Re $2^{\mathbb{N}}$: Agreed, but I wasn't aware that's anything more than a "distinction without a difference". $x\in\mathcal{P}\omega\leftrightarrow f(i)=\left\{{1(i\in x)}\atop{0(i\not\in x)}\right.\ \in\ 2^{\mathbb{N}}$
John Forkosh
<domain-theory>
Is there an isomorphism between universal domains $\mathcal{P}\omega$ and the interval domain $\mathbf{I}\mathbb{R}$?
John Forkosh
# Is there an isomorphism between universal domains $\mathcal{P}\omega$ and the interval domain $\mathbf{I}\mathbb{R}$?

(Asked by: username_0 on 2021-11-05)

Is there a constructive way to one-to-one associate elements $x\in\mathcal{P}\omega$ with elements ${\scriptstyle\mathbf I}\in\mathbf{I}\mathbb{R}$ ?  
I assumed there should be since they're both universal (so kind of an embedding-embedding pair, so to speak), but haven't been able to figure out how it could be done, nor google a solution.

**Edit:** Re comment How do you constructively embed $\mathcal{P}(\{0,1,2\})$ into the interval domain?...  
    Well, here's what I'd been thinking to do for $\mathcal{P}\omega$ in general, which doesn't work as a bijection, but which maybe vaguely works as an embedding. It's all kind of fast-and-loose in the spirit of Stoy's remark about "fiddling with sets of integers" (last paragraph on pg.116 in his book).  
    First let's consider your definition $\mathbf{I}\mathbb{R} = \{[a,b] \mid a, b \in \mathbb{R}\_{[0,1]} \land a \leq b \}$ restricted to $\mathbb{R}\_{[0,1]}=\{r\in\mathbb{R}\mid 0\leq r\leq1\}$. Then for $x\in\mathcal{P}\omega$, first, for each $i\in x$, use the **inverse** pairing function $\mathbb{N}\times\mathbb{N}\to\mathbb{N}$, e.g., <https://en.wikipedia.org/wiki/Pairing_function>, to get $x\to x\_1,x\_2$. Now use the usual construction $x\subseteq\mathbb{N}\to r\_x=\sum\_{i\in x}\frac1{2^i}\in\mathbb{R}\_{[0,1]}$. So now we have $x\in\mathcal{P}\omega\to r\_{x\_1},r\_{x\_2}$, with which we associate the interval $[r\_{\_\mbox{lo}},r\_{\_\mbox{hi}}]$, choosing the lesser of $r\_{x\_1},r\_{x\_2}$ for $r\_{\_\mbox{lo}}$ and ditto for hi. And those $r$'s will be rational if $x$ is finite, and computable/constructive if it's r.e.  
    Second, if it's really necessary to consider $\mathbb{R}$ rather than just $\mathbb{R}\_{[0,1]}$, then for any $x\in\mathcal{P}\omega$, first get $x\_1,x\_2$ as above, but now separate each into its even and odd numbers, i.e., $x\_1^e=\{\frac i2\mid i\in x\_1\land i\mbox{ even}\}$ and $x\_1^o=\{\frac{i+1}2\in x\_1\mid i\mbox{ odd}\}$. And now use $x\_1^e$ to determine the integer part of $r\_{x\_1}$ as $\sum\_{i\in x\_1^e}2^i$, and use $x\_1^o$ to determine the decimal part as above.

**Tags:** domain-theory

> **Comments:**
> **username_1**: Is this supposed to be an isomorphism of underlying sets (any bijection), or an isomorphism of posets (monotone), or an isomorphism of domains (continuous)?  
> **username_1**: Sorry, I misread, you're looking for embeddings, not isomorphisms.  
> **username_1**: Can you embed $P(\{0,1,2\})$ into $\mathrm{I}\mathbb{R}$? Also, please write down the exact definition of $\mathrm{I}\mathbb{R}$.  
> **username_0**: @AndrejBauer Thanks for your several comments. Actually, I was looking for an isomorphism, not just into as implied by "embedding", but also onto (as would have been implied by "projection"). Continuous if possible, but I haven't even been able to construct any bijection, so basically just looking for any ideas. Re $\mathcal{P}(\{0,1,2\})$, of course I can brute-force embed that small set into just about anything, but I'm not seeing any "systematic" way to do it that would extend to $\mathcal{P}\omega$. As for the definition, yeah I've seen several. Choose any you like (continued below...)  
> **username_0**: @AndrejBauer (...continued from above) that permits construction of a bijection. I've personally been mostly trying to use Chapter 7 of Stoltenberg-Hansen, et al, https://books.google.com/books/about/?id=epb39s2wgt0C But, e.g., http://www.entcs.org/mislove/oxford06.pdf is fine if it more easily permits construction of a bijection. Again...just looking for ideas how it might be done.  
> **username_1**: Really? How do you **constructively** embed $P(\{0,1,2\})$ into the interval domain? And I think it's still important that you write down what you think the constructive interval domain is. Do you use Cauchy reals, Dedekind reals, or lower and upper Dedekind cuts? It may matter.  
> **username_0**: @AndrejBauer Re "Really?..." above. I edited the question to illustrate what I'd been very loosely playing around with for $\mathcal{P}\omega$. And with respect to that, I suppose that the interval domain is what you said in your answer, and its constructive elements are those intervals whose lower,upper bounds are computable reals (whether or not that subset actually comprises a subdomain isn't immediately clear to me).  
> **username_1**: Your edit is not using $\mathcal{P}(\omega)$ but $2^{\mathbb{N}}$.  
> **username_0**: @AndrejBauer Re $2^{\mathbb{N}}$: Agreed, but I wasn't aware that's anything more than a "distinction without a difference". $x\in\mathcal{P}\omega\leftrightarrow f(i)=\left\{{1(i\in x)}\atop{0(i\not\in x)}\right.\ \in\ 2^{\mathbb{N}}$  

---

## 1 answers

### Answer by username_1 on 2021-11-06. Score: 7 | Accepted answer

This is only half an answer, but allow me to clear up a constructive point about the interval domain.

The usual definition of the interval domain is
$$\mathrm{I}\mathbb{R} = \{[a,b] \mid a, b \in \mathbb{R} \land a \leq b \} \cup \{\mathbb{R}\},
$$
ordered by reverse inclusion. If we try to use this definition constructively, we get stuck when showing that it is a dcpo. Even showng that an increasing sequence has a supremum is impossible (because constructively it may not be the case that a bounded increasing sequence of reals has a supremum).

The correct constructive definition of the interval domain goes as follows. An element of $\mathrm{I}\mathbb{R}$ is a pair $(L, U) \in P(\mathbb{Q}) \times P(\mathbb{Q})$ such that

1. $L$ is lower and rounded: $p \in L \iff \exists q \in L \,.\, p < q$.
2. $U$ is upper and rounded: $q \in U \iff \exists p \in U \,.\, p < q$.
3. $L$ and $U$ are disjoint.

The ordering is defined by
$$
(L,U) \sqsubseteq (L', U')
\iff
L \subseteq L' \land U \subseteq U'.
$$
Think of $L$ and $U$ as the endpoints of the interval, given respectively as a lower and an upper Dedekind cut. Note that $\emptyset$ is allowed as a cut. It represents either $-\infty$ or $\infty$, for instance $(\emptyset, \emptyset)$ is the bottom element, $(\emptyset, U)$ represents an interval $(-\infty, u]$, and $(L, \emptyset)$ represents an interval $[\ell, \infty)$.

Clearly, we have an inclusion $\mathrm{I}\mathbb{R} \subseteq P(\mathbb{Q}) \times P(\mathbb{Q})$, and since
$$
P(\mathbb{Q}) \times P(\mathbb{Q}) \cong
P(\mathbb{Q} + \mathbb{Q}) \cong
P(\omega),
$$
we have an inclusion $\mathrm{I}\mathbb{R} \to P(\omega)$. The other direction I am still thinking about.

It is also quite clear that the two domains are not isomorphic posets, as $P(\omega)$ is an algebraic lattice but $\mathrm{I}\mathbb{R}$ is not.

**Supplemental:** I cannot tell from your question what precisely you are trying to do, but perhaps you will find [Cartesian closed categories of separable Scott domains](https://doi.org/10.1016/j.tcs.2014.02.042) relevant. There we find invariants, namely *coherence numbers*, that determine when one universal domain embeds into another.

> **Comments:**
> **username_0**: Thanks. Okay, I see your point that the computable subset of $\mathbf{I}\mathbb{R}$ won't be a subdomain (i.e., the "whether or not" part of my comment above should just be "not"). And thanks also for the more formal analysis than anything that had come to mind for me. It all makes me realize that I should have omitted "constructive" in the original question (I should maybe just be interested in the computable elements of each domain, and maybe an isomorphism between those subsets).  
> **username_1**: That won't work either. The computable elements form *effective* domains (you get the c.e. sets instead of $P(\omega)$ and the computble interval domain). These are not computably isomorphic as domains because, again, one is algebraic and the other is not.  
> **username_1**: Do you have an idea that any two universal domains ought to be isomorphic? Because that is not true.  
> **username_1**: I linked to a paper that classifies universal separable Scott domains up to retraction, perhaps that will be relevant to your work.  
> **username_0**: Re "idea that any two universal domains ought to be isomorphic": isomorphic is apparently too strong, but what had crossed my mind is that given any two universal domains $\mathcal{U}_1$ and $\mathcal{U}_2$, and any domain $D$, then there always exist retractions $\hat{r}_1:\mathcal{U}_1\to D$ and $\hat{r}_2:\mathcal{U}_2\to D$. So we can always say $\hat{r}_1\sim\hat{r}_2$ in some way, whereby the two collections of retractions are related in some way, hopefully a strong way, which hopefully extends to $\mathcal{U}_1$ and $\mathcal{U}_2$ themselves. But I hadn't carried this idea any further.  
> **username_0**: Re "link to ccc's of separable Scott domains": Thanks for the link. Have only just briefly scanned it so far, and looks very interesting, so I'll be taking a deeper dive. And re "relevant to your work", maybe "work" is too strong a word. I'm only just self-studying all this stuff. The question/idea wasn't intended to be "research level", per se. But this group seems to be the only computer science group with a "domain theory" tag.  
> **username_1**: If a an object $U$ is universal in the sense that there is a retraction $X \to U$ from every other object, then of course, given any two universal objects there will be retractions between them. Moreover, if we let $R(X)$ be the poset of retracts of $X$, then for universal objects $U_1$ and $U_2$, the posets $R(U_1)$ and $R(U_2)$ are equivalent. For sufficiently nice notion of domain and "retract", it may even happen that $R(X)$ is itself a domain, in which case we can say even more.  

---

