We introduce a new setting, the category of $\omega$PAP spaces, for reasoning denotationally about expressive differentiable and probabilistic programming languages. Our semantics is general enough to assign meanings to most practical probabilistic and differentiable programs, including those that use general recursion, higher-order functions, discontinuous primitives, and both discrete and continuous sampling. But crucially, it is also specific enough to exclude many pathological denotations, enabling us to establish new results about both deterministic differentiable programs and probabilistic programs. In the deterministic setting, we prove very general correctness theorems for automatic differentiation and its use within gradient descent. In the probabilistic setting, we establish the almost-everywhere differentiability of probabilistic programs' trace density functions, and the existence of convenient base measures for density computation in Monte Carlo inference. In some cases these results were previously known, but required detailed proofs with an operational flavor; by contrast, all our proofs work directly with programs' denotations.

翻译：我们引入了一个新框架——$\omega$PAP空间范畴——用于对表达性强的可微和概率编程语言进行指称推理。该语义具有充分的通用性，能够为大多数实际概率与可微程序赋予含义，包括使用一般递归、高阶函数、非连续基元以及离散和连续采样的程序。但关键的是，它也足够具体，能够排除许多病态指称，从而使我们能为确定型可微程序和概率程序建立新结论。在确定型场景中，我们证明了关于自动微分及其在梯度下降中应用的非常通用的正确性定理。在概率场景中，我们建立了概率程序迹密度函数的几乎处处可微性，以及蒙特卡洛推断中密度计算所需便捷基础测度的存在性。部分结论此前虽已知晓，但需要具有操作风格的详细证明；相比之下，我们所有的证明都直接基于程序的指称进行推导。