 |
 |
Special Issue on "Domain Theory and its Applications"
Editors: Michel Schellekens, Achim Jung
1. Mixed powerdomains for probability and nondeterminism
We consider mixed powerdomains combining ordinary nondeterminism and probabilistic nondeterminism. We characterise them as free algebras for suitable (in)equation-al theories; we establish functional representation theorems; and we show equivalencies between state transformers and appropriately healthy predicate transformers. The extended nonnegative reals serve as `truth-values'. As usual with powerdomains, everything comes in three flavours: lower, upper, and order-convex. The powerdomains are suitable convex sets of subprobability valuations, corresponding to resolving nondeterministic choice before probabilistic choice. Algebraically this corresponds to the probabilistic choice operator distributing over the nondeterministic choice operator. (An alternative approach to combining the two forms of nondeterminism would be to resolve probabilistic choice first, arriving at a domain-theoretic version of random sets. However, as we also show, the algebraic approach then runs into difficulties.) Rather than working directly with valuations, we take a domain-theoretic functional-analytic approach, employing domain-theoretic abstract convex sets called Kegelspitzen; these are equivalent to the abstract probabilistic algebras of Graham and Jones, but are more convenient to work with. So we define power Kegelspitzen, and consider free algebras, functional representations, and predicate transformers. To do so we make use of previous work on domain-theoretic cones (d-cones), […]
2. A Few Notes on Formal Balls
Using the notion of formal ball, we present a few new results in the theory of quasi-metric spaces. With no specific order: every continuous Yoneda-complete quasi-metric space is sober and convergence Choquet-complete hence Baire in its $d$-Scott topology; for standard quasi-metric spaces, algebraicity is equivalent to having enough center points; on a standard quasi-metric space, every lower semicontinuous $\bar{\mathbb{R}}_+$-valued function is the supremum of a chain of Lipschitz Yoneda-continuous maps; the continuous Yoneda-complete quasi-metric spaces are exactly the retracts of algebraic Yoneda-complete quasi-metric spaces; every continuous Yoneda-complete quasi-metric space has a so-called quasi-ideal model, generalizing a construction due to K. Martin. The point is that all those results reduce to domain-theoretic constructions on posets of formal balls.
3. The Ho-Zhao Problem
Given a poset $P$, the set, $\Gamma(P)$, of all Scott closed sets ordered by inclusion forms a complete lattice. A subcategory $\mathbf{C}$ of $\mathbf{Pos}_d$ (the category of posets and Scott-continuous maps) is said to be $\Gamma$-faithful if for any posets $P$ and $Q$ in $\mathbf{C}$, $\Gamma(P) \cong \Gamma(Q)$ implies $P \cong Q$. It is known that the category of all continuous dcpos and the category of bounded complete dcpos are $\Gamma$-faithful, while $\mathbf{Pos}_d$ is not. Ho & Zhao (2009) asked whether the category $\mathbf{DCPO}$ of dcpos is $\Gamma$-faithful. In this paper, we answer this question in the negative by exhibiting a counterexample. To achieve this, we introduce a new subcategory of dcpos which is $\Gamma$-faithful. This subcategory subsumes all currently known $\Gamma$-faithful subcategories. With this new concept in mind, we construct the desired counterexample which relies heavily on Johnstone's famous dcpo which is not sober in its Scott topology.
4. The sequential functionals of type $(\iota \rightarrow \iota)^n \rightarrow \iota$ form a dcpo for all $n \in \Bbb N$
We prove that the sequential functionals of some fixed types at type level 2, taking finite sequences of unary functions as arguments, do form a directed complete partial ordering. This gives a full characterisation of for which types the partially ordered set of sequential functionals has this property. As a tool, we prove a normal form theorem for the finite sequential functionals of the types in question,
5. Domains via approximation operators
In this paper, we tailor-make new approximation operators inspired by rough set theory and specially suited for domain theory. Our approximation operators offer a fresh perspective to existing concepts and results in domain theory, but also reveal ways to establishing novel domain-theoretic results. For instance, (1) the well-known interpolation property of the way-below relation on a continuous poset is equivalent to the idempotence of a certain set-operator; (2) the continuity of a poset can be characterized by the coincidence of the Scott closure operator and the upper approximation operator induced by the way below relation; (3) meet-continuity can be established from a certain property of the topological closure operator. Additionally, we show how, to each approximating relation, an associated order-compatible topology can be defined in such a way that for the case of a continuous poset the topology associated to the way-below relation is exactly the Scott topology. A preliminary investigation is carried out on this new topology.
6. Uniqueness of directed complete posets based on Scott closed set lattices
In analogy to a result due to Drake and Thron about topological spaces, this paper studies the dcpos (directed complete posets) which are fully determined, among all dcpos, by their lattices of all Scott-closed subsets (such dcpos will be called $C_{\sigma}$-unique). We introduce the notions of down-linear element and quasicontinuous element in dcpos, and use them to prove that dcpos of certain classes, including all quasicontinuous dcpos as well as Johnstone's and Kou's examples, are $C_{\sigma}$-unique. As a consequence, $C_{\sigma}$-unique dcpos with their Scott topologies need not be bounded sober.
7. The recursion hierarchy for PCF is strict
We consider the sublanguages of Plotkin's PCF obtained by imposing some bound k on the levels of types for which fixed point operators are admitted. We show that these languages form a strict hierarchy, in the sense that a fixed point operator for a type of level k can never be defined (up to observational equivalence) using fixed point operators for lower types. This answers a question posed by Berger. Our proof makes substantial use of the theory of nested sequential procedures (also called PCF Böhm trees) as expounded in the recent book of Longley and Normann.
8. Probabilistic call by push value
We introduce a probabilistic extension of Levy's Call-By-Push-Value. This extension consists simply in adding a " flipping coin " boolean closed atomic expression. This language can be understood as a major generalization of Scott's PCF encompassing both call-by-name and call-by-value and featuring recursive (possibly lazy) data types. We interpret the language in the previously introduced denotational model of probabilistic coherence spaces, a categorical model of full classical Linear Logic, interpreting data types as coalgebras for the resource comonad. We prove adequacy and full abstraction, generalizing earlier results to a much more realistic and powerful programming language.
9. Web spaces and worldwide web spaces: topological aspects of domain theory
Web spaces, wide web spaces and worldwide web spaces (alias C-spaces) provide useful generalizations of continuous domains. We present new characterizations of such spaces and their patch spaces, obtained by joining the original topology with a second topology having the dual specialization order; these patch spaces possess good convexity and separation properties and determine the original web spaces. The category of C-spaces is concretely isomorphic to the category of fan spaces; these are certain quasi-ordered spaces having neighborhood bases of fans, obtained by deleting a finite number of principal dual ideals from a principal dual ideal. Our approach has useful consequences for domain theory, because the T$_0$ web spaces are exactly the generalized Scott spaces of locally approximating ideal extensions, and the T$_0$ C-spaces are exactly the generalized Scott spaces of globally approximating and interpolating ideal extensions. We extend the characterization of continuous lattices as meet-continuous lattices with T$_2$ Lawson topology and the Fundamental Theorem of Compact Semilattices to non-complete posets. Finally, cardinal invariants like density and weight of the involved objects are investigated.
10. Topological Scott Convergence Theorem
Recently, J. D. Lawson encouraged the domain theory community to consider the scientific program of developing domain theory in the wider context of $T_0$ spaces instead of restricting to posets. In this paper, we respond to this calling with an attempt to formulate a topological version of the Scott Convergence Theorem, i.e., an order-theoretic characterisation of those posets for which the Scott-convergence $\mathcal{S}$ is topological. To do this, we make use of the $\mathcal{ID}$ replacement principle to create topological analogues of well-known domain-theoretic concepts, e.g., $\mathcal{I}$-continuous spaces correspond to continuous posets, as $\mathcal{I}$-convergence corresponds to $\mathcal{S}$-convergence. In this paper, we consider two novel topological concepts, namely, the $\mathcal{I}$-stable spaces and the $\mathcal{DI}$ spaces, and as a result we obtain some necessary (respectively, sufficient) conditions under which the convergence structure $\mathcal{I}$ is topological.
11. Convexity and Order in Probabilistic Call-by-Name FPC
Kegelspitzen are mathematical structures coined by Keimel and Plotkin, in order to encompass the structure of a convex set and the structure of a dcpo. In this paper, we ask ourselves what are Kegelspitzen the model of. We adopt a categorical viewpoint and show that Kegelspitzen model stochastic matrices onto a category of domains. Consequently, Kegelspitzen form a denotational model of pPCF, an abstract functional programming language for probabilistic computing. We conclude the present work with a discussion of the interpretation of (probabilistic) recursive types, which are types for entities which might contain other entities of the same type, such as lists and trees.