Skip to main content

Questions tagged [domain-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4 votes
2 answers
222 views

Denotational semantics of intersection types

Is there a denotational (possibly, domain theoretic) semantics of intersection types? If yes, could you provide some references? Let me try to give some context to my question. In the usual ...
LaR's user avatar
  • 335
11 votes
2 answers
370 views

What are pertinent references to cite on Scott domains?

Scott domains are often presented as having been introduced in 1969. However, the first (but numerous!) papers are from the 1970s, so it is not easy to know what the pertinent references are. My two ...
sparusaurata's user avatar
1 vote
2 answers
128 views

Do realizable systems always have some non-well-founded sets?

Suppose we are standing outside a realizable system which admits CZF or a similar constructive set theory. Then consider the following: LEM is not realized (e.g. this MSE answer) The traditional ...
Corbin's user avatar
  • 271
5 votes
2 answers
197 views

Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories

In Atkey & McBride ICFP 2013, they extend a simple type theory with guarded recursion indexed by clock variables $\triangleright^k$ and a clock quantification $\forall k. A$ that conveniently ...
Max New's user avatar
  • 1,695
6 votes
1 answer
278 views

An analogue of Scott continuity for infinite-time-Turing-computable functions

$\newcommand{\tb}{2_{\!\bot}}\newcommand{\tbO}{\tb^{\,\omega}}$Let $2 = \{0,1\}$ and $\tb = \{0,\bot,1\}$. Scott continuity is important for defining models of lambda calculus, a formalism for ...
Jozef Mikušinec's user avatar
7 votes
1 answer
198 views

Is there an isomorphism between universal domains $\mathcal{P}\omega$ and the interval domain $\mathbf{I}\mathbb{R}$?

Is there a constructive way to one-to-one associate elements $x\in\mathcal{P}\omega$ with elements ${\scriptstyle\mathbf I}\in\mathbf{I}\mathbb{R}$ ? I assumed there should be since they're both ...
John Forkosh's user avatar
4 votes
0 answers
56 views

Coinduction principle for smash products of pointed cpos

In "Relational Properties of Domains", Pitts gives a coinduction principle for pointed cpos (cppos). In corollary 6.13 (below), he specializes it to cppos constructed as fixed points of cppo-...
Ryan Kavanagh's user avatar
3 votes
0 answers
106 views

What conditions are necessary (and sufficient) for the order-dual of a Scott-Ershov domain to also be a domain?

That is, considering the underlying poset of a domain, when does the order-dual poset also comprise a domain? Below's a little, not strictly necessary, elaboration of that question. Usual ...
John Forkosh's user avatar
6 votes
1 answer
147 views

Given a domain, how do we build a language whose denotation is the domain?

Say we have an arbitrary domain $D$ with a countable basis $B$. Now, how do i build a "language" whose "denotation" lives in the domain? My understanding is that Dana Scott ...
Siddharth Bhat's user avatar
6 votes
1 answer
316 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 ...
Max New's user avatar
  • 1,695
1 vote
0 answers
195 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 ...
Nathan BeDell's user avatar
7 votes
1 answer
212 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/...
John Forkosh's user avatar
8 votes
0 answers
375 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]...
Yufei Cai's user avatar
  • 161
2 votes
0 answers
56 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$ ...
zander's user avatar
  • 21
19 votes
3 answers
641 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 ...
SorcererofDM's user avatar
7 votes
1 answer
142 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 ...
Basil's user avatar
  • 371
5 votes
1 answer
188 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-...
Basil's user avatar
  • 371
10 votes
3 answers
594 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 ...
fritzo's user avatar
  • 265
5 votes
2 answers
1k 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 ...
Basil's user avatar
  • 371
7 votes
2 answers
217 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 ...
Blaisorblade's user avatar
  • 2,069
8 votes
0 answers
182 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-...
user21929's user avatar
  • 181
12 votes
1 answer
202 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 = \...
Uday Reddy's user avatar
  • 4,796
14 votes
4 answers
887 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 <...
Russell O'Connor's user avatar
16 votes
1 answer
759 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 ...
Charles Stewart's user avatar
7 votes
2 answers
210 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 ...
Robin Green's user avatar
12 votes
1 answer
379 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 ...
Neel Krishnaswami's user avatar
12 votes
1 answer
472 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 ...
Ben 's user avatar
  • 871
11 votes
3 answers
1k 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 ...
Ohad Kammar's user avatar
  • 2,687
13 votes
0 answers
265 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 ...
Neel Krishnaswami's user avatar