6
$\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?

Improve this question
$\endgroup$
12
  • 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
    Commented Sep 17, 2020 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
    Commented Sep 17, 2020 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
    Commented Sep 17, 2020 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
    Commented Sep 17, 2020 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
    Commented Sep 18, 2020 at 13:13

1 Answer 1

Reset to default
6
$\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.

Improve this answer
$\endgroup$
2
  • 1
    $\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
    Commented Sep 20, 2020 at 16:56
  • 2
    $\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
    Commented Sep 20, 2020 at 17:10

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.