面向统计概率编程的领域理论
计算机科学中的逻辑
2021-08-02 v3 编程语言
摘要
我们为具有递归高阶类型、连续概率分布与软约束的语言给出了充分的指称语义。这些是构建计算统计与机器学习中所用贝叶斯模型的极具表达力的语言。其中包括无类型语言，类似于 Church 与 WebPPL，因为我们的语义允许递归混合变元数据类型。我们的语义证明了包括交换性在内的重要程序等价性。我们新的语义模型基于“拟 Borel 预域”。这些是链完全偏序（cpo）与拟 Borel 空间的混合。拟 Borel 空间是近期的概率论模型，聚焦于可容许随机元素之集合。概率在传统上于 cpo 模型中借助概率幂域处理，但已知其在任何具有高阶函数的 cpo 类上均非交换。相比之下，拟 Borel 预域同时支持交换的概率幂域与高阶函数。如我们所展示，拟 Borel 预域既构成 Fiore 公理化领域理论的模型，也构成 Kock 综合测度论的模型。
引用
@article{arxiv.1811.04196,
title = {A Domain Theory for Statistical Probabilistic Programming},
author = {Matthijs Vákár and Ohad Kammar and Sam Staton},
journal= {arXiv preprint arXiv:1811.04196},
year = {2021}
}