<p>As it turns out, the OP is interested in the <em>specific</em> case of the interval domain. Martín Escardó's PhD thesis &quot;<a href="http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-374/index.html" rel="noreferrer">PCF extended with real numbers: a domain-theoretic approach to higher-order exact real number computation</a>&quot; extends the programming language PCF with a datatype of reals whose denotation is the interval domain.</p>

CC BY-SA 4.0
2020-09-20T16:56:36.293Z
Could you also add a note about the general case, upto as much as you figured out about the general case?
Siddharth Bhat
CC BY-SA 4.0
2020-09-20T17:10:11.673Z
The general case is a bit involved, I might do it if I get a spare moment and some inspiration. It look like a rabbit hole to me.
Andrej Bauer
CC BY-SA 4.0
2020-09-19T23:05:25.620Z
2020-09-19T23:05:25.620Z
Andrej Bauer
<p>Say we have an arbitrary domain <span class="math-container">$D$</span> with a countable basis <span class="math-container">$B$</span>. Now, how do i build a &quot;language&quot; whose &quot;denotation&quot; lives in the domain?</p>
<p>My understanding is that Dana Scott initially built domains to get a model of typed lambda calculus. Then, people bgan studing domains in their own right. So if I know that something forms a domain, can I &quot;extract computation&quot; / &quot;extract a language&quot; out of it?</p>
<p>Perhaps said differently, does every domain <span class="math-container">$D$</span> [with more conditions as necessary] always come equipped with the structure of a closed cartesian category?</p>

CC BY-SA 4.0
2020-09-17T14:53:26.637Z
Your last sentence does not make much sense, because a domain is not a category.  I mean, of course, as a poset, it is a category in a trivial way, but then being cartesian closed would mean that the domain is a Heyting algebra, which I don't think happens very often (I'm not even sure it's possible).
Damiano Mazza
CC BY-SA 4.0
2020-09-17T14:57:33.260Z
I think you might be confusing between the fact that the category of domains is a particular cartesian closed category (CCC) and the fact that the $\lambda$-calculus is the "internal language" of CCCs.  This means that every CCC $\mathbf C$ induces a $\lambda$-calculus, which will be the usual simply-typed $\lambda$-calculus plus lots of constants for each arrow of $\mathbf C$, and the behavior of these constants is given by composition in $\mathbf C$.
Damiano Mazza
CC BY-SA 4.0
2020-09-17T16:26:05.227Z
Yes, I do believe I am confused. Let me write up what I currently understand. I can solve domain equations of the form $D \simeq V \oplus [D \rightarrow D]$ [$D$ unknown], thereby giving me domain $D^\star$ which satisfies the above equation. Thus $D^*$ models 'lambda calculus' over $V$. I'm asking about the _inverse_ problem, I think. Given some domain $D_0$, does there exist a $V_0$ such that $D_0 \simeq V_0 \oplus [D_0 \rightarrow D_0]$? Or perhaps the domain models "imperative languages", and I should solve $D_0 \simeq V_0 \oplus [I \rightarrow D_0]$ for some index set $I$ [the store].
Siddharth Bhat
CC BY-SA 4.0
2020-09-17T16:26:32.430Z
In general, if I have _some_ domain, how can I "recover" the computational model behind the domain? Is this even a well-posed question?
Siddharth Bhat
CC BY-SA 4.0
2020-09-17T22:03:13.897Z
I have it on good authority that Dana Scott invented domain theory to dissuade people from using the untyped $\lambda$-calculus, and discovered later that the domains also model the untyped $\lambda$-calculus. So you have a bit of imaginary history in there.
Andrej Bauer
CC BY-SA 4.0
2020-09-17T22:09:59.343Z
A single domain is like a datatype in a programming language, so you should be asking: *Given a domain $D$, how do I enrich the simply-typed $\lambda$-calculus with a datatype whose denotation is $D$?* And to make this a well-posed problem, we should assume that $D$ is an effective domain. The answer is positive but also boring, because we adjoin to the programming langauge a new datatype `D` and enough operations to capture the structure of $D$.
Andrej Bauer
CC BY-SA 4.0
2020-09-18T10:21:48.470Z
@AndrejBauer Thank you. How do I know whether I've added 'enough operations' to capture the structure of $D$? Can we make this precise?
Siddharth Bhat
CC BY-SA 4.0
2020-09-18T13:13:49.830Z
An effective domain $D$ is described by (computable) enumeration $b : \mathbb{N} \to D_0$ of its compact elements, and some other conditions too long to be listed here. We would adjoin to the calculus a primitive type `D` whose denotation is $D$, and for every compact element $b_k \in D_0$ a constant `b_k` of type `D`, or perhaps a single constant `b : nat → D`. We would also need something that gives us suprema of compact elements (typically fixpoint operators do in concrete cases). But the details are not clear to me, I'd have to actually think about it. It won't be terribly interesting.
Andrej Bauer
CC BY-SA 4.0
2020-09-18T14:43:23.877Z
To be concrete, does that mean that one a language whose datatypes are 'spacetime intervals', because the paper 'A Domain of Spacetime Intervals in General Relativity' constructs a domain of intervals in spacetime. (https://link.springer.com/article/10.1007/s00220-006-0066-5). I believe that one can enumerate these intervals, since the entire 'space of spacetime intervals' is compact, and thus must have a finite open cover.
Siddharth Bhat
CC BY-SA 4.0
2020-09-19T07:08:58.683Z
You should have been concrete from the beginning, because if you are really interested in a specific case then much more can be said about it. In your case, you are asking about (a variant of) the *interval domain*. See [Martín Escardó's PhD thesis](http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-374/index.html) which describes RealPCF, the programming language PCF extended with the interval domain.
Andrej Bauer
CC BY-SA 4.0
2020-09-19T14:09:06.390Z
Thank you! I was interested in the broader question, hoping to apply it to the narrower question at hand. You're right; I should have specified both in the original text.
Siddharth Bhat
CC BY-SA 4.0
2020-09-19T14:09:28.877Z
If you are willing to submit an answer, I will be glad to mark it accepted, both to close this question as answered, and for the points.
Siddharth Bhat
<ct.category-theory><denotational-semantics><domain-theory>
Given a domain, how do we build a language whose denotation is the domain?
Siddharth Bhat
# Given a domain, how do we build a language whose denotation is the domain?

(Asked by: username_0 on 2020-09-15)

Say we have an arbitrary domain $D$ with a countable basis $B$. Now, how do i build a "language" whose "denotation" lives in the domain?

My understanding is that Dana Scott initially built domains to get a model of typed lambda calculus. Then, people bgan studing domains in their own right. So if I know that something forms a domain, can I "extract computation" / "extract a language" out of it?

Perhaps said differently, does every domain $D$ [with more conditions as necessary] always come equipped with the structure of a closed cartesian category?

**Tags:** ct.category-theory, denotational-semantics, domain-theory

> **Comments:**
> **username_1**: Your last sentence does not make much sense, because a domain is not a category.  I mean, of course, as a poset, it is a category in a trivial way, but then being cartesian closed would mean that the domain is a Heyting algebra, which I don't think happens very often (I'm not even sure it's possible).  
> **username_1**: I think you might be confusing between the fact that the category of domains is a particular cartesian closed category (CCC) and the fact that the $\lambda$-calculus is the "internal language" of CCCs.  This means that every CCC $\mathbf C$ induces a $\lambda$-calculus, which will be the usual simply-typed $\lambda$-calculus plus lots of constants for each arrow of $\mathbf C$, and the behavior of these constants is given by composition in $\mathbf C$.  
> **username_0**: Yes, I do believe I am confused. Let me write up what I currently understand. I can solve domain equations of the form $D \simeq V \oplus [D \rightarrow D]$ [$D$ unknown], thereby giving me domain $D^\star$ which satisfies the above equation. Thus $D^*$ models 'lambda calculus' over $V$. I'm asking about the _inverse_ problem, I think. Given some domain $D_0$, does there exist a $V_0$ such that $D_0 \simeq V_0 \oplus [D_0 \rightarrow D_0]$? Or perhaps the domain models "imperative languages", and I should solve $D_0 \simeq V_0 \oplus [I \rightarrow D_0]$ for some index set $I$ [the store].  
> **username_0**: In general, if I have _some_ domain, how can I "recover" the computational model behind the domain? Is this even a well-posed question?  
> **username_2**: I have it on good authority that Dana Scott invented domain theory to dissuade people from using the untyped $\lambda$-calculus, and discovered later that the domains also model the untyped $\lambda$-calculus. So you have a bit of imaginary history in there.  
> **username_2**: A single domain is like a datatype in a programming language, so you should be asking: *Given a domain $D$, how do I enrich the simply-typed $\lambda$-calculus with a datatype whose denotation is $D$?* And to make this a well-posed problem, we should assume that $D$ is an effective domain. The answer is positive but also boring, because we adjoin to the programming langauge a new datatype `D` and enough operations to capture the structure of $D$.  
> **username_0**: @AndrejBauer Thank you. How do I know whether I've added 'enough operations' to capture the structure of $D$? Can we make this precise?  
> **username_2**: An effective domain $D$ is described by (computable) enumeration $b : \mathbb{N} \to D_0$ of its compact elements, and some other conditions too long to be listed here. We would adjoin to the calculus a primitive type `D` whose denotation is $D$, and for every compact element $b_k \in D_0$ a constant `b_k` of type `D`, or perhaps a single constant `b : nat → D`. We would also need something that gives us suprema of compact elements (typically fixpoint operators do in concrete cases). But the details are not clear to me, I'd have to actually think about it. It won't be terribly interesting.  
> **username_0**: To be concrete, does that mean that one a language whose datatypes are 'spacetime intervals', because the paper 'A Domain of Spacetime Intervals in General Relativity' constructs a domain of intervals in spacetime. (https://link.springer.com/article/10.1007/s00220-006-0066-5). I believe that one can enumerate these intervals, since the entire 'space of spacetime intervals' is compact, and thus must have a finite open cover.  
> **username_2**: You should have been concrete from the beginning, because if you are really interested in a specific case then much more can be said about it. In your case, you are asking about (a variant of) the *interval domain*. See [Martín Escardó's PhD thesis](http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-374/index.html) which describes RealPCF, the programming language PCF extended with the interval domain.  
> **username_0**: Thank you! I was interested in the broader question, hoping to apply it to the narrower question at hand. You're right; I should have specified both in the original text.  
> **username_0**: If you are willing to submit an answer, I will be glad to mark it accepted, both to close this question as answered, and for the points.  

---

## 1 answers

### Answer by username_2 on 2020-09-19. Score: 6 | Accepted answer

As it turns out, the OP is interested in the *specific* case of the interval domain. Martín Escardó's PhD thesis "[PCF extended with real numbers: a domain-theoretic approach to higher-order exact real number computation](http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-374/index.html)" extends the programming language PCF with a datatype of reals whose denotation is the interval domain.

> **Comments:**
> **username_0**: Could you also add a note about the general case, upto as much as you figured out about the general case?  
> **username_2**: The general case is a bit involved, I might do it if I get a spare moment and some inspiration. It look like a rabbit hole to me.  

---

