5
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ 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). $\endgroup$ – Damiano Mazza Sep 17 '20 at 14:53
  • 1
    $\begingroup$ 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$. $\endgroup$ – Damiano Mazza Sep 17 '20 at 14:57
  • 2
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 17 '20 at 22:03
  • 2
    $\begingroup$ 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$. $\endgroup$ – Andrej Bauer Sep 17 '20 at 22:09
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 18 '20 at 13:13
4
$\begingroup$

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" extends the programming language PCF with a datatype of reals whose denotation is the interval domain.

$\endgroup$
  • $\begingroup$ Could you also add a note about the general case, upto as much as you figured out about the general case? $\endgroup$ – Siddharth Bhat Sep 20 '20 at 16:56
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 20 '20 at 17:10

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.