A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism
A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism
复制标题
DOI：
10.1016/j.entcs.2019.09.016
复制
发表时间：
2019-11
期刊：
影响因子：
--
通讯作者：
Di Wang;Jan Hoffmann;T. Reps
中科院分区：
文献类型：
--
作者：
Di Wang;Jan Hoffmann;T. Reps
概率编程是一种越来越流行的建模随机性和不确定性的形式主义。为概率程序设计语义模型已经得到了广泛的研究，但在技术上具有挑战性。当试图解释（i）非结构化的控制流时，会出现特殊的复杂性，这是低级命令式程序中的一个自然特征;（ii）一般递归，一种广泛使用的编程范式;（iii）非确定性，它通常用于表示概率模型中的对抗行为，并支持基于细化的开发。本文提出了一个指称语义框架，支持上述三个功能，同时允许以不同的方式处理非确定性。为了同时支持概率选择和非确定性选择，给出了控制流图的语义。语义遵循代数方法：它可以以不同的方式实例化，只要某些代数属性成立。特别地，语义可以被实例化以支持程序状态或状态转换器之间的非确定性。我们发展了一个新的形式化的非确定性的基础上powerdomainsoversub-probability核。权力域中的语义对象享有我们称之为广义凸性的概念，它是凸性的推广。作为一个应用程序，本文勾勒出一个代数框架的概率程序，这已经提出了一个配套文件中的静态分析。
Probabilistic programming is an increasingly popular formalism for modeling randomness and uncertainty. Designing semantic models for probabilistic programs has been extensively studied, but is technically challenging. Particular complications arise when trying to account for (i) unstructured control-flow, a natural feature in low-level imperative programs; (ii) general recursion, an extensively used programming paradigm; and (iii) nondeterminism, which is often used to represent adversarial actions in probabilistic models, and to support refinement-based development. This paper presents a denotational-semantics framework that supports the three features mentioned above, while allowing nondeterminism to be handled in different ways. To support both probabilistic choice and nondeterministic choice, the semantics is given over control-flowhyper-graphs. The semantics follows analgebraicapproach: it can be instantiated in different ways as long as certain algebraic properties hold. In particular, the semantics can be instantiated to support nondeterminism among eitherprogram statesorstate transformers. We develop a new formalization of nondeterminism based onpowerdomainsoversub-probability kernels. Semantic objects in the powerdomain enjoy a notion we callgeneralized convexity, which is a generalization of convexity. As an application, the paper sketches an algebraic framework for static analysis of probabilistic programs, which has been proposed in a companion paper.