同伦类型论中用于概率编程的综合拓扑
计算机科学中的逻辑
2022-05-17 v2 范畴论
摘要
ALEA Coq 库基于集合范畴上 Giry 单子的一个变体形式化了测度论。这使得能够解释具有从离散分布采样原语的概率编程语言。然而，连续分布必须被离散化，因为其相应测度无法在其 carriers 的所有子集上定义。本文提出使用综合拓扑为类型论中的概率计算建模连续分布。我们研究了任意集合上的初始 -frame 及相应的诱导拓扑。基于这些内蕴拓扑，我们定义了集合上的 valuation 与下积分，并证明了 Riesz 定理与 Fubini 定理的若干版本。随后我们展示了如何构造 Lebesgue valuation，从而构造连续分布。
引用
@article{arxiv.1912.07339,
title = {Synthetic topology in Homotopy Type Theory for probabilistic programming},
author = {Martin E. Bidlingmaier and Florian Faissole and Bas Spitters},
journal= {arXiv preprint arXiv:1912.07339},
year = {2022}
}