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.
翻译:从选择及其产生的成本与回报角度描述系统,有望让算法设计者和程序员无需具体说明如何做出选择;在实现中,这些选择可通过优化技术来实现,并越来越多地借助机器学习方法。我们从编程语言视角研究这一方法。定义了两个支持决策抽象的小型语言:一个包含选择与回报,另一个在此基础上增加了概率。我们给出了操作语义和指称语义。针对第二个语言,我们考虑了三种指称语义,分别对应程序可能值与期望回报之间的不同程度相关性。操作语义将标准构造的常规语义与对可能执行策略空间的优化相结合。具有组合性的指称语义依赖于选择单子来处理选择,并辅以另一个单子来处理其他效应(如回报或概率)。我们建立了充分性定理,证明两种语义在所有情况下均一致。我们还证明了在基本类型上的完全抽象性,其中概率情况下的观测概念随不同程度的相关性而变化。我们给出了选择与回报及概率结合的公理,并针对不含概率的回报情形建立了基本类型上的完全性。