Smart Choices and the Selection Monad
Martín Abadi, Gordon D. Plotkin
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper2
- Handling the Selection MonadGordon D. Plotkin, Ningning XiePLDI 2025 · 被引用 1 次
- Scaling Optimization over Uncertainty via CompilationMinsung Cho, John Gouwar, Steven HoltzenOOPSLA 2025 · 被引用 1 次
它引用的顶会 Paper4
- Interaction trees: representing recursive and impure programs in CoqLi-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur 等POPL 2020 · 被引用 133 次
- A simple differentiable programming languageMartín Abadi, Gordon D. PlotkinPOPL 2020 · 被引用 49 次
- Backpropagation in the simply typed lambda-calculus with linear negationAloïs Brunel, Damiano Mazza, Michele PaganiPOPL 2020 · 被引用 24 次
- From Multisets over Distributions to Distributions over MultisetsBart JacobsLICS 2021 · 被引用 23 次
相关 Paper
- Full abstraction for the quantum lambda-calculusPierre Clairambault, Marc de VismePOPL 2020 · 被引用 25 次
- Denotational Foundations for Expected Cost AnalysisPedro H. Azevedo de AmorimOOPSLA 2025 · 被引用 4 次
- Commutative Monads for Probabilistic Programming LanguagesXiaodong Jia, Bert Lindenhovius, Michael W. Mislove, Vladimir ZamdzhievLICS 2021 · 被引用 19 次
- Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic ChoiceAlejandro Aguirre, Lars BirkedalPOPL 2023 · 被引用 13 次
- Combining Nondeterminism, Probability, and Termination: Equational and Metric ReasoningMatteo Mio, Ralph Sarkis, Valeria VignudelliLICS 2021 · 被引用 14 次
