A type theory for probability density functions
A type theory for probability density functions
复制标题
概率密度函数的类型论
DOI：
10.1145/2103656.2103721
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Alexander G. Gray
中科院分区：
文献类型：
--
作者：
Sooraj Bhat;Ashish Agarwal;R. Vuduc;Alexander G. Gray
人们对创建概率编程语言以简化统计任务的编码产生了极大的兴趣;然而，仍然不存在一种同时提供（1）连续概率分布、（2）自然表达自定义概率模型的能力和（3）的正式语言。概率密度函数（PDF）。这些特征的集合对于基本统计技术的机械化是必要的。我们形式化的第一个概率语言，表现出这些功能，它作为一个基础框架扩展的想法，更一般的语言。特别新颖的是我们的类型系统绝对连续（AC）的分布（那些允许PDF）和我们的PDF计算程序，计算PDF的一大类AC分布。我们的形式化铺平了道路，对强大的统计重构的严格编码。
There has been great interest in creating probabilistic programming languages to simplify the coding of statistical tasks; however, there still does not exist a formal language that simultaneously provides (1) continuous probability distributions, (2) the ability to naturally express custom probabilistic models, and (3) probability density functions (PDFs). This collection of features is necessary for mechanizing fundamental statistical techniques. We formalize the first probabilistic language that exhibits these features, and it serves as a foundational framework for extending the ideas to more general languages. Particularly novel are our type system for absolutely continuous (AC) distributions (those which permit PDFs) and our PDF calculation procedure, which calculates PDF s for a large class of AC distributions. Our formalization paves the way toward the rigorous encoding of powerful statistical reformulations.