17 votes

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 ...
user avatar
  • 26.7k
10 votes
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 ...
user avatar
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. ...
user avatar
10 votes

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 ...
user avatar
  • 13.2k
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. ...
user avatar
  • 26.7k
7 votes
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" ([1], Sect. 12.3): (I) each compact element dominates finitely many elements. The above condition is the defining property of Berry'...
user avatar
6 votes
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 ...
user avatar
  • 26.7k
6 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 ...
user avatar
  • 668
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 \...
user avatar
  • 26.7k
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 ...
user avatar
  • 26.7k
4 votes

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 ...
user avatar
  • 1,512
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 ...
user avatar
4 votes

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 ...
user avatar
3 votes
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 ...
user avatar
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 ...
user avatar
  • 1,910
2 votes
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 ...
user avatar
2 votes

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

Well, Mislove's quote already contains a positive answer: the category of dcpos is carteisan closed and also closed under the probabilistic powerdomain. It can indeed be used to give a denotational ...
user avatar
1 vote

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

That definition implies that there is no required unique bottom in a predomain, i.e. each down set (reverse chain) could have a distinct least element, but that there is no necessary least element for ...
user avatar
  • 2,874

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