高阶概率论的一个方便范畴
A Convenient Category for Higher-Order Probability Theory
摘要：
高阶概率程序设计语言允许程序员以简洁和结构化的方式编写机器学习和统计学中的复杂模型，但超出了概率论的标准度量理论形式化。程序可以同时使用高阶函数和连续分布，甚至可以定义函数的概率分布。但是标准概率论不能很好地处理高阶函数：可测空间的范畴不是笛卡尔封闭的。在这里，我们引入拟Borel空间。我们表明，这些空间：形成一个新的形式化的概率论取代可测空间;形成一个carnival封闭的范畴，因此支持高阶函数;形成一个很好的指向的范畴，因此支持良好的证明原则的方程推理;和支持连续的概率分布。我们证明了使用准Borel空间的高阶函数和概率：表明一个著名的建设概率论涉及随机函数获得一个清洁的表达;和推广的Finetti定理，这是一个重要的定理在概率论，准Borel空间。
英文摘要：
Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory does not handle higher-order functions well: the category of measurable spaces is not cartesian closed. Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti's theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
