一句话:本文构造并刻画多重集单子到分布单子的分配律,统一非确定性与概率语义并应用于采样语义。
在编程语言语义中,如何同时建模非确定性与概率性长期是难题;Plotkin 早已指出幂集单子与分布单子之间不存在分配律。本文转向多重集单子与分布单子,详细阐述多重集单子到分布单子的分配律,并揭示多重集与概率分布之间的丰富理论。作者提出“平行多项分布律”,给出至少四种等价定义,说明它通过并行放置多项分布实现,并与超几何分布交换。进一步证明该分配律与多重集上一种新的 zipping 操作相容;抽象上,这可理解为固定大小多重集函子在提升到分布单子的 Kleisli 范畴后具有的幺半结构。文中还给出该理论在采样语义中的应用。
A well-known challenge in the semantics of programming languages is how to combine non-determinism and probability. At a technical level, the problem arises from the fact that there is a no distributive law between the powerset monad and the distribution monad - as noticed some twenty years ago by Plotkin. More recently, it has become clear that there is a distributive law of the multiset monad over the distribution monad. This article elaborates the details of this distributivity and shows that there is a rich underlying theory relating multisets and probability distributions. It is shown that the new distributive law, called parallel multinomial law, can be defined in (at least) four equivalent ways. It involves putting multinomial distributions in parallel and commutes with hypergeometric distributions. Further, it is shown that this distributive law commutes with a new form of zipping for multisets. Abstractly, this can be described in terms of monoidal structure for a fixed-size multiset functor, when lifted to the Kleisli category of the distribution monad. Concretely, an application of the theory to sampling semantics is included.