On probabilistic termination of functional programs with continuous distributions
On probabilistic termination of functional programs with continuous distributions
复制标题
DOI：
10.1145/3453483.3454111
复制
发表时间：
2021-04
期刊：
影响因子：
--
通讯作者：
Raven Beutner;Luke Ong
中科院分区：
文献类型：
--
作者：
Raven Beutner;Luke Ong
我们研究具有递归、随机条件和连续分布抽样的高阶概率函数程序的终止。关于具有连续分布的程序的终止概率的推理是困难的，因为终止执行的枚举不能提供任何非平凡的界限。我们提出了一个新的操作语义的基础上的痕迹的间隔，这是健全的和完整的标准采样为基础的语义，其中（可数）枚举可以提供任意紧的下界。因此，我们得到的第一个证明，决定几乎必然终止（AST）的连续分布的程序是1020-完全（对于CbN）。我们还提供了一个组合表示我们的语义的交叉类型系统。在第二部分中，我们提出了一种证明非仿射程序的AST的方法，即，递归程序，可以在递归体的计算期间，从不同的调用位置进行多次递归调用（一阶函数）。与确定性语言不同，递归调用站点的数量对终止概率有直接影响。我们的框架支持一个证明系统，可以验证AST的程序远远超出了现有方法的范围。我们已经构建了原型实现我们的方法计算下限的终止概率，AST验证。
We study termination of higher-order probabilistic functional programs with recursion, stochastic conditioning and sampling from continuous distributions. Reasoning about the termination probability of programs with continuous distributions is hard, because the enumeration of terminating executions cannot provide any non-trivial bounds. We present a new operational semantics based on traces of intervals, which is sound and complete with respect to the standard sampling-based semantics, in which (countable) enumeration can provide arbitrarily tight lower bounds. Consequently we obtain the first proof that deciding almost-sure termination (AST) for programs with continuous distributions is Π20-complete (for CbN). We also provide a compositional representation of our semantics in terms of an intersection type system. In the second part, we present a method of proving AST for non-affine programs, i.e., recursive programs that can, during the evaluation of the recursive body, make multiple recursive calls (of a first-order function) from distinct call sites. Unlike in a deterministic language, the number of recursion call sites has direct consequences on the termination probability. Our framework supports a proof system that can verify AST for programs that are well beyond the scope of existing methods. We have constructed prototype implementations of our methods for computing lower bounds on the termination probability, and AST verification.