We define a probabilistic programming language for Gaussian random variables with a first-class exact conditioning construct. We give operational, denotational and equational semantics for this language, establishing convenient properties like exchangeability of conditions. Conditioning on equality of continuous random variables is nontrivial, as the exact observation may have probability zero; this is Borel's paradox. Using categorical formulations of conditional probability, we show that the good properties of our language are not particular to Gaussians, but can be derived from universal properties, thus generalizing to wider settings. We define the Cond construction, which internalizes conditioning as a morphism, providing general compositional semantics for probabilistic programming with exact conditioning.

翻译：我们定义高西亚随机变量的概率性编程语言,使用一流的精确调节结构。我们为高西亚随机变量提供操作性、省略性和等式语义,为该语言提供操作性、分解性和等式语义,建立像条件互换性那样的方便性。对连续随机变量的平等性进行限定是非边际的,因为确切的观察可能为概率零;这是博雷尔的悖论。使用有条件概率的绝对公式,我们表明我们语言的良好性能不是高西亚人所特有的,而是来自普遍特性,因此可以推广到更广泛的环境。我们定义Cond 构造,它将内化为形态,为精确调节的概率编程提供一般的构成性语义。