We define a monad on the category of complete metric spaces with short maps, which assigns to each space the space of Radon probability measures on it with finite first moment, equipped with the Kantorovich--Wasserstein distance. It is analogous to the Giry monad on the category of Polish spaces, and it extends a construction due to van Breugel for compact and for 1-bounded complete metric spaces. We prove that this Kantorovich monad arises from a colimit construction on finite powers, which formalizes the intuition that probability measures are limits of finite samples. The proof relies on a new criterion for when an ordinary left Kan extension of lax monoidal functors is a monoidal Kan extension. This colimit characterization allows for the development of integration theory and other things, such as the treatment of measures on spaces of measures, completely without measure theory. We also show that the category of algebras of the Kantorovich monad is equivalent to the category of closed convex subsets of Banach spaces with short affine maps as the morphisms.
Dec 15 2017 cs.LO
Imprecise and incomplete specification of system \textitconfigurations threatens safety, security, functionality, and other critical system properties and uselessly enlarges the configuration spaces to be searched by configuration engineers and auto-tuners. To address these problems, this paper introduces \textitinterpreted formalisms based on real-world types for configurations. Configuration values are lifted to values of real-world types, which we formalize as \textitsubset types in Coq. Values of these types are dependent pairs whose components are values of underlying Coq types and proofs of additional properties about them. Real-world types both extend and further constrain \textitmachine-level configurations, enabling richer, proof-based checking of their consistency with real-world constraints. Tactic-based proof scripts are written once to automate the construction of proofs, if proofs exist, for configuration fields and whole configurations. \textitFailures to prove reveal real-world type errors. Evaluation is based on a case study of combinatorial optimization of Hadoop performance by meta-heuristic search over Hadoop configurations spaces.
Various extensions of public announcement logic have been proposed with quantification over announcements. The best-known extension is called arbitrary public announcement logic, APAL. It contains a primitive language construct Box phi intuitively expressing that 'after every public announcement of a formula, formula phi is true.' The logic APAL is undecidable and it has an infinitary axiomatization. Now consider restricting the APAL quantification to public announcements of boolean formulas only, such that Box phi intuitively expresses that 'after every public announcement of a boolean formula, formula phi is true.' This logic can therefore called boolean arbitrary public announcement logic, BAPAL. The logic BAPAL is the subject of this work. It is decidable and it has a finitary axiomatization. These results may be considered of interest, as for various applications quantification over booleans is sufficient in formal specifications.