Probabilistic completion of nondeterministic models

Abstract

Motivated by Moggi's work [34] on how monads can be used to capture computational behavior, there has been a growing interest in finding monads which capture the precise computational effects generated when combining the theory of probabilistic choice and the theory of nondeterministic choice. The resulting theory, called here the theory of mixed choice [23, 31, 33], captures the interaction between the two choice operators by requiring appropriate distributivity axioms (probabilistic choice over nondeterministic choice), in addition to the operations and axioms from both individual choice theories. Classically, the required monad has been defined by composing the adjunctions on the left hand side of the following diagram.* This requires the composition of the distributions functor Dfin , which constructs free models of probabilistic choice over an arbitrary set X, and the finite convex set functor Cvxfin , which constructs free models of mixed choice over an arbitrary convex set (C, +lambda), as seen in [31, 33, 49]. This construction allows us to build a free mixed choice model from an arbitrary model for probabilistic (P) choice, in such fashion as to preserve the P choice model's probabilistic structure. We consider the dual approach to the above algorithm. Through general categorical results from Barr and Wells [2], we observed that free models for mixed choice could also be constructed over arbitrary models of nondeterministic (ND) choice. This allows for an alternative algorithm for constructing models for mixed choice, which corresponds to going up the right hand side of the above commuting diagram. This requires the composition of the finite nonempty powerset functor P*fin , which constructs free models of nondeterministic choice over an arbitrary set X, and the ∨-stable functor Stblfin, which constructs free models of mixed choice over an arbitrary semilattice (S, ∨). This alternative approach allows for a wider range of mixed choice models to be studied: those that would arise from arbitrary semilattices, hence arbitrary nondeterministic models with a possible non-standard definition of nondeterminism. By abstract categorical notions, it is known that the ∨-stable functor Stblfin exists (the functor in the N-E corner of the above diagram). However, up until now there have been no concrete presentations of this functor, nor any notion of how to construct free mixed choice models over arbitrary semilattices. These concepts represent the main focus of this thesis. We motivate and develop a new property for convex sets generated over a set equipped with a semilattice structure. This notion is called ∨- stability. In essence, a ∨-stable convex set preserves the ND structure on its underlying set (i.e., if it contains an element s such that x ∨ y = s, then it must also contain the convex subset generated by x and y). Finally, we generalize many of our results in two directions. First, we construct the corresponding ∨-stable functors for infinitary mixed choice theories over Set. We then extend the entire development of the thesis to express posetal model categories (i.e over Poset) of our theories. This would include constructing models for mixed choice over models obtained from the convex (Plotkin), lower (Hoare), and upper (Smyth) variants of nondeterminism. Furthermore, we prove that the results in the literature obtained by following the left-hand side of the given diagram are equivalent to our results obtained by traversing its right-hand side. *Please refer to dissertation for diagram.