In this paper we systematically derive a predicate transformer semantics from a direct semantics for a simple probabilistic-nondeterministic programming language . This goal is achieved by exhibiting the direct semantics as isomorphic to a continuation semantics from which the predicate transformer semantics can be read off immediately. This isomorphism allows one to identify nonempty convex compact saturated sets of valuations on the set S of states with certain “good” functionals from to in a way similar to the one how H. (...) Minkowski in 1903 related nonempty convex compact subsets of to what is nowadays called Minkowski functionals. (shrink)

In this article we give a general categorical construction via reflection functors for various completions of T0-spaces subordinate to sobrification, with a particular emphasis on what we call the -completion, a type of directed completion introduced by Wyler [O. Wyler, Dedekind complete posets and Scott topologies, in: B. Banaschewski, R.-E. Hoffmann , Continuous Lattices Proceedings, Bremen 1979, in: Lecture Notes in Mathematics, vol. 871, Springer Verlag, 1981, pp. 384–389]. A key result is that all completions of a certain type are (...) universal, hence unique . We give a direct definition of the -completion and develop its theory by introducing a variant of the Scott topology, which we call the d-topology. For partially ordered sets the -completion turns out to be a natural dcpo-completion that generalizes the rounded ideal completion. In the latter part of the paper we consider settings in which the -completion agrees with the sobrification respectively the closed ideal completion. (shrink)