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.

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