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 ...
- 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 ...
- 4,823
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.
...
- 601
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 ...
- 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.
...
- 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'...
- 4,823
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 ...
- 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 ...
- 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 \...
- 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 ...
- 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 ...
- 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 ...
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 ...
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 ...
- 4,823
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 ...
- 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 ...
- 633
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 ...
- 21
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 ...
- 2,874
Only top scored, non community-wiki answers of a minimum length are eligible