A Formalized Hierarchy of Probabilistic System Types - Proof Pearl
A Formalized Hierarchy of Probabilistic System Types - Proof Pearl
复制标题
概率系统类型的形式化层次结构 - Proof Pearl
DOI：
10.1007/978-3-319-22102-1_13
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Andreas Lochbihler
中科院分区：
文献类型：
--
作者：
Johannes Hölzl;Andreas Lochbihler
在文献中研究了许多概率系统的模型。余代数被用来将它们划分为系统类型并比较它们的表达能力。在这项工作中，我们正式的概率系统类型的层次结构在伊莎贝尔/HOL建模的语义不同的系统作为codatestries。这种方法产生了简单而简洁的证明，因为双相似性与codatestries的相等一致。在此过程中，我们开发了有界集和离散概率分布的库，并将它们与（共同）数据类型定义的设施相结合。
Numerous models of probabilistic systems are studied in the literature. Coalgebra has been used to classify them into system types and compare their expressiveness. In this work, we formalize the resulting hierarchy of probabilistic system types in Isabelle/HOL by modeling the semantics of the different systems as codatatypes. This approach yields simple and concise proofs, as bisimilarity coincides with equality for codatatypes. On the way, we develop libraries of bounded sets and discrete probability distributions and integrate them with the facility for (co)datatype definitions.
登录
查看更多内容
DOI：
10.1016/s1571-0661(04)80632-7
发表时间：
2003-07
期刊：
--
影响因子：
--
作者：
F. Bartels;A. Sokolova;E. Vink
通讯作者：
F. Bartels;A. Sokolova;E. Vink
为什么我们不能在 HOL 中使用 SML 风格的数据类型声明
DOI：
10.1016/b978-0-444-89880-7.50042-5
发表时间：
1992
期刊：
J. Log. Comput.
影响因子：
--
作者：
Elsa L. Gunter
通讯作者：
Elsa L. Gunter
在 Coq 中实现高性能类别理论库的经验
DOI：
10.1007/978-3-319-08970-6_18
发表时间：
2014
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jason Gross;A. Chlipala;David I. Spivak
通讯作者：
David I. Spivak
见证（Co）数据类型
DOI：
10.1007/978-3-662-46669-8_15
发表时间：
2015
期刊：
影响因子：
--
作者：
Jasmin Christian Blanchette;Andrei Popescu;Dmitriy Traytel
通讯作者：
Dmitriy Traytel
经过验证的概率密度函数编译器
DOI：
10.1007/978-3-662-46669-8_4
发表时间：
2015
期刊：
ArXiv
影响因子：
--
作者：
Manuel Eberl;Johannes Hölzl;Tobias Nipkow
通讯作者：
Tobias Nipkow