Smart Choices and the Selection Monad

TL;DR

This paper explores decision-making abstractions in programming languages using the selection monad, providing semantics and axioms for choices, rewards, and probabilities to facilitate optimization and machine learning integration.

Contribution

It introduces two small languages with decision-making features, develops their semantics using the selection monad, and proves adequacy and full abstraction results.

Findings

Operational and denotational semantics coincide

Full abstraction established at base types

Axioms for choice, rewards, and probability are complete

Abstract

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, rely on the selection monad, to handle choice, augmented 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 base 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 base types for the case of rewards without probability.