一句话:在 DCPO 范畴上构造三种概率可交换单子,并为概率不动点演算给出可靠且充分的指称语义。
概率编程语言的指称语义长期缺少 DCPO 范畴上的概率可交换单子。本文构造了三种这样的单子,并给出可继续生成更多单子的通用构造。作者用这些单子为概率不动点演算(PFPC)建立可靠且充分的指称语义;PFPC 是带混合变型递归类型、项递归与概率选择的按值调用简单类型 lambda 演算。文章进一步证明,在连续 dcpo 的特殊情形下,三种单子都等同于 Jones 的 valuation 单子,并完整刻画其诱导的 Eilenberg-Moore 范畴,证明它们均同构于 Keimel 与 Plotkin 的连续 Kegelspitzen 范畴。
A long-standing open problem in the semantics of programming languages supporting probabilistic choice is to find a commutative monad for probability on the category DCPO. In this paper we present three such monads and a general construction for finding even more. We show how to use these monads to provide a sound and adequate denotational semantics for the Probabilistic FixPoint Calculus (PFPC) - a call-by-value simply-typed lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. We also show that in the special case of continuous dcpo's, all three monads coincide with the valuations monad of Jones, and we fully characterise the induced Eilenberg-Moore categories by showing that they are all isomorphic to the category of continuous Kegelspitzen of Keimel and Plotkin.