Smart Choices and the Selection Monad

Describing systems in terms of choices and their resulting costs and rewards offers the promise of freeing algorithm designers and programmers from specifying how those choices should be made; in implementations, the choices can be realized by optimization techniques and, increasingly, by machine learning methods. We study this approach from a programming-language perspective. We define two small languages that support decision-making abstractions: one with choices and rewards, and the other additionally with probabilities. We give both operational and denotational semantics. In the case of the second language we consider three denotational semantics, with varying degrees of correlation between possible program values and expected rewards. The operational semantics combine the usual semantics of standard constructs with optimization over spaces of possible execution strategies. The denotational semantics, which are compositional and can also be viewed as an implementation by translation to a simpler language, rely on the selection monad, to handle choice, combined with an auxiliary monad, to handle other effects such as rewards or probability. We establish adequacy theorems that the two semantics coincide in all cases. We also prove full abstraction at ground types, with varying notions of observation in the probabilistic case corresponding to the various degrees of correlation. We present axioms for choice combined with rewards and probability, establishing completeness at ground types for the case of rewards without probability.