Probabilistic programming languages aid developers performing Bayesian inference. These languages provide programming constructs and tools for probabilistic modeling and automated inference. Prior work introduced a probabilistic programming language, ProbZelus, to extend probabilistic programming functionality to unbounded streams of data. This work demonstrated that the delayed sampling inference algorithm could be extended to work in a streaming context. ProbZelus showed that while delayed sampling could be effectively deployed on some programs, depending on the probabilistic model under consideration, delayed sampling is not guaranteed to use a bounded amount of memory over the course of the execution of the program. In this paper, we the present conditions on a probabilistic program's execution under which delayed sampling will execute in bounded memory. The two conditions are dataflow properties of the core operations of delayed sampling: the $m$-consumed property and the unseparated paths property. A program executes in bounded memory under delayed sampling if, and only if, it satisfies the $m$-consumed and unseparated paths properties. We propose a static analysis that abstracts over these properties to soundly ensure that any program that passes the analysis satisfies these properties, and thus executes in bounded memory under delayed sampling.

翻译：概率性编程语言帮助开发者进行巴耶斯推断。 这些语言为概率性模型和自动推断提供了编程构造和工具。 先前的工作引入了概率性编程语言ProbZelus, 将概率性编程功能扩大到无边界的数据流。 这项工作表明,延迟取样推算算法可以扩展至在流流环境中工作。 ProbZelus 显示, 虽然延迟取样可以在某些程序上有效部署, 取决于所考虑的概率性模型, 延迟取样不能保证在程序执行过程中使用一定数量的内存。 在本文中, 我们目前执行概率性方案的条件, 延迟取样将在封闭性记忆中执行。 这两个条件是延迟取样核心操作的数据流特性: 美元假设属性和未分离的路径属性。 一个程序在延迟取样中执行约束性记忆, 如果它能够满足所估计的美元和不可分离的路径的内存量, 则不能保证在程序执行过程中使用一定的内存量。 我们提议在精确性模型中进行固定性分析, 对这些特性进行精确性分析, 进行这些精确性分析。