Much work has been done to give semantics to probabilistic programming languages. In recent years, most of the semantics used to reason about probabilistic programs fall in two categories: semantics based on Markov kernels and semantics based on linear operators. Both styles of semantics have found numerous applications in reasoning about probabilistic programs, but they each have their strengths and weaknesses. Though it is believed that there is a connection between them there are no languages that can handle both styles of programming. In this work we address these questions by defining a two-level calculus and its categorical semantics which makes it possible to program with both kinds of semantics. From the logical side of things we see this language as an alternative resource interpretation of linear logic, where the resource being kept track of is sampling instead of variable use.
翻译:已经做了很多工作来给概率性编程语言提供语义。 近年来, 多数用于解释概率性程序的理由的语义学都分为两类: 基于 Markov 内核的语义学和基于线性操作员的语义学。 两种语义学在概率性编程的推理中都发现了许多应用, 但两者都有各自的长处和弱点。 虽然人们认为它们之间没有能够同时处理两种编程风格的语言联系。 在这项工作中,我们通过定义两个层次的语义学及其绝对的语义学来解决这些问题,从而可以用两种语义进行编程。 从逻辑的角度来看,我们把这个语言看作是线性逻辑的替代资源解释, 在那里, 资源被保存的追踪是抽样而不是变量的使用。</s>