Smart Choices and the Selection Monad
Martín Abadi, Gordon D. Plotkin
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.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 68c8e937-38e4-4f4d-bb54-8f5244a862d2Cited by top-tier papers2
- Handling the Selection MonadGordon D. Plotkin, Ningning XiePLDI 2025 · 1 citation
- Scaling Optimization over Uncertainty via CompilationMinsung Cho, John Gouwar, Steven HoltzenOOPSLA 2025 · 1 citation
Builds on4
- Interaction trees: representing recursive and impure programs in CoqLi-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur et al.POPL 2020 · 133 citations
- A simple differentiable programming languageMartín Abadi, Gordon D. PlotkinPOPL 2020 · 49 citations
- Backpropagation in the simply typed lambda-calculus with linear negationAloïs Brunel, Damiano Mazza, Michele PaganiPOPL 2020 · 24 citations
- From Multisets over Distributions to Distributions over MultisetsBart JacobsLICS 2021 · 23 citations
Related papers
- Full abstraction for the quantum lambda-calculusPierre Clairambault, Marc de VismePOPL 2020 · 25 citations
- Denotational Foundations for Expected Cost AnalysisPedro H. Azevedo de AmorimOOPSLA 2025 · 4 citations
- Commutative Monads for Probabilistic Programming LanguagesXiaodong Jia, Bert Lindenhovius, Michael W. Mislove, Vladimir ZamdzhievLICS 2021 · 19 citations
- Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic ChoiceAlejandro Aguirre, Lars BirkedalPOPL 2023 · 13 citations
- Combining Nondeterminism, Probability, and Termination: Equational and Metric ReasoningMatteo Mio, Ralph Sarkis, Valeria VignudelliLICS 2021 · 14 citations
