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.
翻译:大量工作致力于为概率编程语言赋予语义。近年来,用于推理概率程序的大多数语义可分为两类:基于马尔可夫核的语义和基于线性算子的语义。这两种语义风格在概率程序推理中均得到广泛应用,但各有优劣。尽管人们认为两者之间存在联系,但目前尚不存在能同时处理这两种编程风格的语言。本研究通过定义一个双层演算及其范畴语义来解决这些问题,使得我们能够用这两种语义进行编程。从逻辑角度而言,我们将该语言视为线性逻辑的一种替代资源解释,其中被追踪的资源是采样而非变量使用。