7
$\begingroup$

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.
   

$\endgroup$
9
  • 1
    $\begingroup$ Is this supposed to be an isomorphism of underlying sets (any bijection), or an isomorphism of posets (monotone), or an isomorphism of domains (continuous)? $\endgroup$ Commented Nov 5, 2021 at 13:02
  • 1
    $\begingroup$ Sorry, I misread, you're looking for embeddings, not isomorphisms. $\endgroup$ Commented Nov 5, 2021 at 14:25
  • 2
    $\begingroup$ Can you embed $P(\{0,1,2\})$ into $\mathrm{I}\mathbb{R}$? Also, please write down the exact definition of $\mathrm{I}\mathbb{R}$. $\endgroup$ Commented Nov 5, 2021 at 14:55
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Nov 6, 2021 at 8:30
  • 1
    $\begingroup$ Your edit is not using $\mathcal{P}(\omega)$ but $2^{\mathbb{N}}$. $\endgroup$ Commented Nov 7, 2021 at 8:49

1 Answer 1

7
$\begingroup$

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 relevant. There we find invariants, namely coherence numbers, that determine when one universal domain embeds into another.

$\endgroup$
7
  • $\begingroup$ 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). $\endgroup$ Commented Nov 7, 2021 at 7:57
  • 2
    $\begingroup$ 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. $\endgroup$ Commented Nov 7, 2021 at 8:47
  • 2
    $\begingroup$ Do you have an idea that any two universal domains ought to be isomorphic? Because that is not true. $\endgroup$ Commented Nov 7, 2021 at 8:48
  • 2
    $\begingroup$ I linked to a paper that classifies universal separable Scott domains up to retraction, perhaps that will be relevant to your work. $\endgroup$ Commented Nov 7, 2021 at 9:23
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Nov 8, 2021 at 13:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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