一句话:证明幂集单子到有限分布单子存在弱分配律,导出凸幂集单子,并应用于概率-非确定系统的迹语义与行为等价。
在指称语义中,同时描述概率选择与非确定性选择长期存在组合困难。从范畴论看,其根源是幂集单子到有限分布单子不存在分配律。本文证明了幂集单子到有限分布单子存在弱分配律。由此,作者将熟知的凸幂集单子重新刻画为幂集单子到凸代数范畴的弱提升。该结果给出了概率与非确定性交互系统的统一语义框架,并用于研究此类系统的迹语义与行为等价。
Combining probabilistic choice and non-determinism is a long standing problem in denotational semantics. From a category theory perspective, the problem stems from the absence of a distributive law of the powerset monad over the distribution monad. In this paper we prove the existence of a weak distributive law of the powerset monad over the finite distribution monad. As a consequence, we retrieve the well-known convex powerset monad as a weak lifting of the powerset monad to the category of convex algebras. We provide applications to the study of trace semantics and behavioral equivalences of systems with an interplay between probability and non-determinism.