一句话：提出随机 λ-演算的布尔值语义，用测度代数解释高阶概率程序并支持等式推理。
本文为高阶概率程序建立语义与推理原则。作者扩展无类型 λ-演算，在 Scott 与 Plotkin 的 λ-理论模型基础上引入随机变量，并重构为基于测度代数的高阶布尔值模型。项被解释为携带无限抛硬币序列的 continuation-style 语义，该序列作为随机性来源。由于 β-归约对无限制项不再可靠，作者引入新的不动点算子作为语法构造。文章还给出若干关键等式，并提出在测度代数中解释项之间的新相等概念，使得可以推理不几乎处处相等的项。该工作为概率程序及其高阶性质提供了新的语义框架与推理方法。
The ordinary untyped λ-calculus has a λ-theoretic model proposed in two related forms by Scott and Plotkin in the 1970s. Recently Scott showed how to introduce probability by extending these models with random variables. However, to reason about correctness and to add further features, it is useful to reinterpret the construction in a higher-order Boolean-valued model involving a measure algebra. We develop the semantics of an extended stochastic λ-calculus suitable for modeling a simple higher-order probabilistic programming language. We exhibit a number of key equations satisfied by the terms of our language. The terms are interpreted using a continuation-style semantics with an additional argument, an infinite sequence of coin tosses, which serves as a source of randomness. We also introduce a fixpoint operator as a new syntactic construct, as β-reduction turns out not to be sound for unrestricted terms. Finally, we develop a new notion of equality between terms interpreted in a measure algebra, allowing one to reason about terms that may not be equal almost everywhere. This provides a new framework and reasoning principles for probabilistic programs and their higher-order properties.
DOI 原文 ·
@inproceedings{paperbot4318,
title = {Boolean-Valued Semantics for the Stochastic λ-Calculus},
author = {Giorgio Bacci and Robert Furber and Dexter Kozen and Radu Mardare and Prakash Panangaden and Dana Scott},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209175}
}