17
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 theoreticians who are not used to developing software. So they usually relegate the task of implementation to students (a notable exception is Norbert Müller's ...
12
An example where $A(x)$ is empty is the set of real numbers $\mathbb{R}$ with the usual ordering. It has no compact elements at all.
If we assume the second condition then $A(x)$ cannot be empty: if $A(x) = \emptyset$ then by the second condition $x$ is the empty join, therefore the least element of $L$, which is compact, therefore $x \in A(x) = \emptyset$, ...
10
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 the past few years there has been a very active line of research around so-called quantitative denotational semantics of linear logic, based on the idea (...
10
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.
An information system $(A,Con,\vdash)$ induces a trivial domain iff it is itself trivial: $Con = \{\emptyset\}$. Otherwise, there exists at least one point ...
10
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 sociological reasons.
I believe the main argument against exact computation of reals is one of performance. So the short answer is, whenever performance is more ...
7
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's dI-domains, which are distributive (that's what the "d" stands for) algebraic domains satisfying condition I. This is a widely known and well studied class ...
6
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 that $U \circ F$ can be equipped with the structure of a monad, as you say.
And yes, predomains need not have a least element.
6
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 above is the supremum of an $\omega$-chain inside $D_i$, so $d_i$ is well defined.
It is an element of $D$ since, by continuity,
$$
\begin{array}{ll}
& f_i(...
6
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 \mathbb{R} \land a \leq b \} \cup \{\mathbb{R}\},
$$
ordered by reverse inclusion. If we try to use this definition constructively, we get stuck when showing that ...
5
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.
4
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 used that tag) use non flat domains.
Maybe you should give examples of domains that are taken as flat,
while it would be better to do differently.
Many problems ...
4
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 appearance in a semantic model is not for proof-theoretic convenience - they represent the strong connection between the model and actual computation.
3
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 the latter there are S0 and SS⊥, and so on. I know that in the early 90s Loïc Colson worked on models using the above interpretation of integers, although I ...
2
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 other pairs $(b,q) \in m$ we have $b \subseteq a$ and $\{p\} \vdash q$.
In other words, a molecule is a mapping that closes off neatly, having a largest pair.
2
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 semantics to higher-order probabilistic computation. However, dcpos fail to satisfy the "usual approximation assumptions" that every element can be approximated ...
2
Proving that λ x. Ω ≠ Ω in is one of the goals Abramsky sets for his lazy lambda calculus theory (page 2 of his paper, already cited by Uday Reddy), because they are both in weak head normal form. As of definition 2.7, he discusses explicitly that eta-reduction λ x. M x → M is not generally valid, but it is possible if M terminates in every environment. ...
2
I am not sure if the Haskell report defines the semantics rigorously enough to settle the question about what $\lambda x.\, \bot$ should mean. However, it is common experience in Haskell as well as all other lazy functional languages, that, if you ask them to evaluate a term that represents $\lambda x.\, \bot$, the evaluation terminates. The "As a ...
1
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 the whole structure.
You could form a domain by appending a bottom under all other least elements, or by identifying all least elements (i.e. say they are ...
Only top voted, non community-wiki answers of a minimum length are eligible