Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

The tag has no usage guidance.

5
votes
1answer
108 views

Does the Category of CPOs have omega^op limits?

In "Domains and Lambdi Calculi" by Amadio and Curien, in the section on solving recursive domain equations (section 7), they give sufficient conditions on a cpo-enriched category so that the category ...
1
vote
0answers
95 views

Have there been any practical applications of domain theory to formal methods?

By Domain Theory, I mean the use of CPOs (or related topological/order-theoretic structures) to study the denotational semantics of programming languages. Compared to the two other common approaches ...
7
votes
1answer
151 views

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

As per subject, if a Scott domain with $T_2$ topology is to be constructed from a Scott information system, then what besides the usual definitional requirements, e.g., https://en.wikipedia.org/wiki/...
9
votes
0answers
183 views

Denotational semantics of System $F_\omega$ with recursive types and general recursion

Is there a denotational semantics for System $F_\omega$ in literature that supports both recursive types and general recursion? I'm looking for a model of Ralf Hinze's variant of System $F_\omega$ [4]...
2
votes
0answers
50 views

Criteria for being below the least fixed point

Given a complete partial order $(D,\, {\leq})$ and a Scott-continuous function $F\colon D \rightarrow D$ and some fixed point $X = F(X)$. Are there any criteria that ensure that $X = \mathsf{lfp} F$ ...
19
votes
3answers
537 views

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

Currently, computation of reals in most popular languages is still done via floating point operations. On the other hand, theories like type two effectivity (TTE) and domain theory have long promised ...
5
votes
1answer
110 views

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

In a poset $(D, \sqsubseteq)$, a compact element is an element $d \in D$ such that for every directed set $A$ which happens to have a supremum $\bigsqcup A \in D$ with $d \sqsubseteq \bigsqcup A$, it ...
5
votes
1answer
171 views

What are Zhang's molecules?

I'm currently looking into the representation theory of Scott domains. In his paper "dI-Domains as prime information systems" (1992), Guo-Qiang Zhang uses prime information systems to represent dI-...
10
votes
3answers
508 views

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

Equivalently, is there a known denotational semantics for probabilistic higher-order functional programming languages? Specifically, is there a domain model of pure untyped $\lambda$-calculus extended ...
5
votes
2answers
287 views

Flat vs non-flat domains

My understanding is that, more often than not, when people use domain theory for higher-type computability or the denotational semantics of functional programming languages, they tend to prefer flat ...
7
votes
2answers
179 views

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

I was reading about Call-by-Push-Value in the introducing paper from 1999, but I have some confusion, partially because of my unfamiliarity with domain theory. I might have figured it out, but I'd ...
8
votes
0answers
168 views

Equivalence of categories of directed complete posets

I asked this question there: https://math.stackexchange.com/questions/700975/equivalence-of-categories-of-directed-complete-posets. Since I had no answer, I try here. In the book ``Domains and Lambda-...
12
votes
1answer
157 views

Is this an equivalent condition for algebraic posets?

The definition of "algebraic poset" in Continuous Lattices and Domains, Definition I-4.2, says that, for all $x \in L$, the set $A(x) = {\downarrow} x \cap K(L)$ should be a directed set, and $x = \...
14
votes
4answers
525 views

Is eta-equivalence for functions compatiable with Haskell's seq operation?

Lemma: Assuming eta-equivalence we have that (\x -> ⊥) = ⊥ :: A -> B. Proof: ⊥ = (\x -> ⊥ x) by eta-equivalence, and <...
16
votes
1answer
641 views

Seeking Scott's original LCF paper

Is the following manuscript publically available? Dana Scott, 1969, A theory of computable functions of higher type. Unpublished seminar notes, 7 pages, University of Oxford. There is a discussion ...
7
votes
2answers
184 views

Prior work on finding domain-theoretic suprema of equivalent total functions?

In slightly more down-to-earth terms, this question is sort of about lazy evaluation in functional programming - except that it's more ambitious in general than just seeking what a typical Haskell ...
11
votes
1answer
338 views

When do coherence spaces have pullbacks and pushouts?

$\newcommand{\symp}{\Bumpeq}$ A coherence relation $\symp_X$ on a set $X$ is a reflexive and symmetric relation. A coherence space is a pair $(X, \symp_X)$, and a morphism $f : X \to Y$ between ...
9
votes
1answer
353 views

In domain theory, what can the extra structure present in metric spaces be used for?

Smyth's chapter in the handbook of logic in computer science and other references describe how metric spaces can be used as domains. I do understand that complete metric spaces give unique fixed ...
10
votes
3answers
900 views

What is a good Category Theory-Domain Theory dictionary?

When dealing with the domain theoretic categories (say CPO and $\omega$CPO), I frequently wish for a dictionary for the language of category theory in domain theory. That is, given a concept, say ...
13
votes
0answers
223 views

Generalizing limit-colimit coincidence to Scott-continuous adjunctions: any uses?

In Abramsky and Jung's 1994 handbook chapter on denotational semantics, after proving that the limit and colimit of expanding sequences exist and coincide, they have the following to say about ...