A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language

In this paper we systematically derive a predicate transformer semantics from a direct semantics for a simple probabilistic-nondeterministic programming language Lp. 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 IS to I in a way similar to the one how H. Minkowski in 1903 related nonempty convex compact subsets of Rn to what is nowadays called Minkowski functionals.