Program Logic for?Higher-Order Probabilistic Programs in?Isabelle/HOL
Program Logic for?Higher-Order Probabilistic Programs in?Isabelle/HOL
复制标题
Isabelle/HOL 中高阶概率程序的程序逻辑
DOI：
10.1007/978-3-030-99461-7_4
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Sato Tetsuya
中科院分区：
文献类型：
--
作者：
Hirata Michikazu;Minamide Yasuhiko;Sato Tetsuya
验证框架PPV（概率程序验证）验证功能概率程序支持高阶函数，连续分布和条件推理。PPV是基于准Borel空间的理论，引入它来给出具有连续分布的高阶概率编程语言的语义。在本文中，我们形式化的准Borel空间的理论和PPV的核心部分在Isabelle/HOL。我们首先在Isabelle/HOL库中的Giry单子的基础上构造了一个准Borel空间上的概率单子。我们的形式化PPV的扩展，使功能的可积性可以正式讨论。最后，我们证明了在我们的机械化PPV的Monte Carlo逼近的可积性和收敛性。
The verification framework PPV (Probabilistic Program Verification) verifies functional probabilistic programs supporting higher-order functions, continuous distributions, and conditional inference. PPV is based on the theory of quasi-Borel spaces which is introduced to give a semantics of higher-order probabilistic programming languages with continuous distributions. In this paper, we formalize a theory of quasi-Borel spaces and a core part of PPV in Isabelle/HOL. We first construct a probability monad on quasi-Borel spaces based on the Giry monad in the Isabelle/HOL library. Our formalization of PPV is extended so that integrability of functions can be discussed formally. Finally, we prove integrability and convergence of the Monte Carlo approximation in our mechanized PPV.