# Tag Info

### Computation of reals: floating point vs TTE vs domain theory vs etc

I work in real-number computation, and I wish I knew the real answer. But I can speculate. It's a sociological problem, I think. The community of people who work on exact real arithmetic consists of ...
Accepted

### Is there any known CCC closed under a probabilistic powerdomain operation?

The following is an extended comment, it does not answer your question in the terms you posed it but does give a semantics for higher-order probabilistic calculi which you may find of interest. In ...
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. ...

### Computation of reals: floating point vs TTE vs domain theory vs etc

In general, people always care about floating point errors. However I disagree with Andrej, and I do not think that floats are preferred to arbitrary precision reals (for the most part) because of ...

### 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. ...
Accepted

### In which posets is the set of compact elements downwards closed?

The only natural condition I can think of is Berry's "I condition" (, Sect. 12.3): (I) each compact element dominates finitely many elements. The above condition is the defining property of Berry'...
Accepted

### Call-by-push-value's denotational semantics of "thunk diverge"

Yes, your reading is correct. $U$ forgets that something is a domain, but does not change the underlying carrier set or the poset structure. The least element is still there. It is also the case ...
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 ...
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 \...
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 ...

### Flat vs non-flat domains

With only flat domains, you cannot define limits to construct "infinite" structures, such as looping structures, for data or for programs. Fixpoint constructions in denotational semantics (since you ...
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 ...

### Is there any known CCC closed under a probabilistic powerdomain operation?

The comment below is correct, but it's important to understand the meaning of "finite" or "compact" elements of a domain. These are the denotations of objects computable in finite time, so their ...
Accepted

### Flat vs non-flat domains

For what concerns the use of non-flat domains, babou already gave examples. I can add that sometimes it may even be useful to see integers as streams: there's ⊥, above which there are 0 and S⊥, above ...

### 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 ...
Accepted

### What are Zhang's molecules?

Restating the definition to make the quantifiers easier to understand: A molecule is a finite stable approximable mapping, such that there exists a largest pair $(a,p) \in m$, such that for all ...