11 votes

What are pertinent references to cite on Scott domains?

I asked Dana Scott who kindly responded. I am relaying his answer: I think the paper “A type-theoretical alternative to ISWIM, CUCH, OWHY” answers the questions and gives the context of the discovery....
Andrej Bauer's user avatar
  • 28.9k
10 votes
Accepted

What else (besides the usual) can be said about a Scott Information System if the constructed domain is required to be Hausdorff?

Since the least element $\bot$ of any Scott domain is a compactification point $-$ the only open set containing it is the whole space $-$ the Scott topology is never Hausdorff, unless it is trivial. ...
Andrew Polonsky's user avatar
7 votes

What are pertinent references to cite on Scott domains?

First papers Scott (1993), A type-theoretical alternative to ISWIM, CUCH, OWHY. This 1969 manuscript was later published in TCS. The title is a bit odd but it seems to hide the very first written ...
7 votes
Accepted

Does the Category of CPOs have omega^op limits?

Here's an attempt (please check!). We have that $\bot_D = d$, where $$ d_i = \bigsqcup^{D_i} \{\bot_i,f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),\ldots\} $$ By construction (and monotonicity), the ...
chi's user avatar
  • 678
7 votes

An analogue of Scott continuity for infinite-time-Turing-computable functions

The domain-theoretic considerations of the kind you are asking about can be carried out using synthetic domain theory. Related to it is syntehtic topology, and in fact the two share many common ideas. ...
Andrej Bauer's user avatar
  • 28.9k
6 votes
Accepted

Is there an isomorphism between universal domains $\mathcal{P}\omega$ and the interval domain $\mathbf{I}\mathbb{R}$?

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 \...
Andrej Bauer's user avatar
  • 28.9k
5 votes
Accepted

Given a domain, how do we build a language whose denotation is the domain?

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 ...
Andrej Bauer's user avatar
  • 28.9k
4 votes
Accepted

Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories

Let me first say that I did not look carefully at the second part of your question, nor your sketch of why the clock quantifier should commute with propositional existential quantification. I will ...
Jonathan Sterling's user avatar
3 votes
Accepted

Do realizable systems always have some non-well-founded sets?

You are using the wrong definition of well-foundedness. Let $R \subseteq A \times A$ be a relation. Consider the following definitions: $R$ is inductive when for all $B \subseteq A$, if $\forall x \...
Andrej Bauer's user avatar
  • 28.9k
2 votes
Accepted

Denotational semantics of intersection types

Intersection types appear in typed programming languages to capture the idea that a given expression may carry multiple functionalities. For example, given a type $\mathsf{read}\;\alpha$ of readable ...
Andrej Bauer's user avatar
  • 28.9k
2 votes

Denotational semantics of intersection types

Later edit: When I wrote the answer below, I was thinking of intersection types as they are understood in the context of the untyped $\lambda$-calculus. It is now clear that this is not the right ...
Damiano Mazza's user avatar
2 votes

Do realizable systems always have some non-well-founded sets?

CZF includes the $\in$-induction axiom, which is the constructively sensible version of the foundation axiom. So everything in one of its models is well-founded in that sense. However, while I'm no ...
Dan Doel's user avatar
  • 1,021
2 votes

Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories

This question sounds related to Transfinite Iris, which proposes to change the Iris model from Nat-indexed propositions to Ordinal-indexed propositions to have "later" commute with ...
gasche's user avatar
  • 2,040

Only top scored, non community-wiki answers of a minimum length are eligible