智能选择与选择单子
Smart Choices and the Selection Monad
AI总结：
从编程语言视角定义两种支持决策抽象的小型语言，基于选择单子给出操作与指称语义，证明两者一致并建立基础类型上的完全抽象与完备性。
摘要：
通过选择及其产生的成本与回报来描述系统，有望使算法设计者和程序员免于指定如何做出这些选择；在实现中，这些选择可以通过优化技术，以及越来越多地通过机器学习方法来实现。我们从编程语言的角度研究这种方法。我们定义了两种支持决策抽象的小型语言：一种包含选择和回报，另一种还额外包含概率。我们给出了两者的操作语义和指称语义。对于第二种语言，我们考虑了三种指称语义，它们在可能的程序值与预期回报之间具有不同程度的相关性。操作语义将标准构造的常规语义与对可能执行策略空间的优化相结合。指称语义是组合式的，依赖于选择单子来处理选择，并辅以辅助单子来处理其他效果，如回报或概率。我们证明了充分性定理，即在所有情况下这两种语义是一致的。我们还在基础类型上证明了完全抽象，在概率情况下，对应于各种相关性的不同观察概念。我们提出了将选择与回报和概率相结合的公理，并在无概率的回报情况下确立了基础类型上的完备性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
