A lambda-calculus foundation for universal probabilistic programming
A lambda-calculus foundation for universal probabilistic programming
复制标题
DOI：
10.1145/2951913.2951942
复制
发表时间：
2015-12
期刊：
影响因子：
--
通讯作者：
J. Borgström;Ugo Dal Lago;A. Gordon;Marcin Szymczak
中科院分区：
文献类型：
--
作者：
J. Borgström;Ugo Dal Lago;A. Gordon;Marcin Szymczak
我们开发了一种具有连续分布和硬约束和软约束的无类型概率λ演算的操作语义，作为通用概率编程语言如教堂、圣公会和风险投资的基础。我们的第一个贡献是通过创建项上的度量空间和定义步进索引近似，将λ演算的经典运算语义适应于连续环境。我们证明了这种基于分布的语义的大步和小步公式的等价性。为了更接近推理技术，我们还将术语的基于采样的语义定义为从随机样本的踪迹到值的函数。我们证明了在迹空间上由积分引起的分布等于基于分布的语义。我们的第二个贡献是将踪迹马尔科夫链蒙特卡罗(MCMC)的实现技术形式化，并证明其正确性。一个关键的步骤是定义由迹MCMC诱导的分布收敛于基于分布的语义的充分条件。据我们所知，这是对于高阶函数式语言或具有软约束的语言的TRACE MCMC的第一个严格的正确性证明。
We develop the operational semantics of an untyped probabilistic λ-calculus with continuous distributions, and both hard and soft constraints,as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of λ-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integration over the space of traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language, or for a language with soft constraints.